∀ (M : Type u_1) (α : Type u_2) [inst : Group M] [inst_1 : MulAction M α] {m n : ℕ}
  [MulAction.IsMultiplyPreprimitive M α n] {s : Set α} [Finite ↑s],
  s.ncard + m = n → MulAction.IsMultiplyPreprimitive (↥(fixingSubgroup M s)) (↥(SubMulAction.ofFixingSubgroup M s)) m