∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {m n : ℕ}
  [AddAction.IsMultiplyPretransitive G α n] (s : Set α) [Finite ↑s],
  s.ncard + m ≤ n →
    ↑n ≤ ENat.card α →
      AddAction.IsMultiplyPretransitive (↥(fixingAddSubgroup G s)) (↥(SubAddAction.ofFixingAddSubgroup G s)) m