∀ {G : Type u_1} [inst : AddMonoid G] {x y : G},
  AddCommute x y →
    IsOfFinAddOrder y →
      (∀ (p : ℕ), Nat.Prime p → p ∣ addOrderOf x → p * addOrderOf x ∣ addOrderOf y) → addOrderOf (x + y) = addOrderOf y