∀ {X : Type u_1} {m₁ : X → X → X} {e₁ : X},
  EckmannHilton.IsUnital m₁ e₁ →
    ∀ [h : AddZeroClass X],
      (∀ (a b c d : X), m₁ (a + b) (c + d) = m₁ a c + m₁ b d) → ∀ (a b c : X), a + b + c = a + (b + c)