∀ {M : Type u_1} [toSemigroup : AddSemigroup M] [toOne : Zero M] (one_mul : ∀ (a : M), 0 + a = a)
  (mul_one : ∀ (a : M), a + 0 = a) (npow : ℕ → M → M) (npow_zero : ∀ (x : M), npow 0 x = 0)
  (npow_succ : ∀ (n : ℕ) (x : M), npow (n + 1) x = npow n x + x) (mul_comm : ∀ (a b : M), a + b = b + a)
  [toIsLeftCancelMul : IsLeftCancelAdd M] [toSemigroup_1 : AddSemigroup M] [toOne_1 : Zero M]
  (one_mul_1 : ∀ (a : M), 0 + a = a) (mul_one_1 : ∀ (a : M), a + 0 = a) (npow_1 : ℕ → M → M)
  (npow_zero_1 : ∀ (x : M), npow_1 0 x = 0) (npow_succ_1 : ∀ (n : ℕ) (x : M), npow_1 (n + 1) x = npow_1 n x + x)
  (mul_comm_1 : ∀ (a b : M), a + b = b + a) [toIsLeftCancelMul_1 : IsLeftCancelAdd M],
  { toAddSemigroup := toSemigroup, toZero := toOne, zero_add := one_mul, add_zero := mul_one, nsmul := npow,
          nsmul_zero := npow_zero, nsmul_succ := npow_succ, add_comm := mul_comm,
          toIsLeftCancelAdd := toIsLeftCancelMul }.toAddCommMonoid =
      { toAddSemigroup := toSemigroup_1, toZero := toOne_1, zero_add := one_mul_1, add_zero := mul_one_1,
          nsmul := npow_1, nsmul_zero := npow_zero_1, nsmul_succ := npow_succ_1, add_comm := mul_comm_1,
          toIsLeftCancelAdd := toIsLeftCancelMul_1 }.toAddCommMonoid →
    { toAddSemigroup := toSemigroup, toZero := toOne, zero_add := one_mul, add_zero := mul_one, nsmul := npow,
        nsmul_zero := npow_zero, nsmul_succ := npow_succ, add_comm := mul_comm,
        toIsLeftCancelAdd := toIsLeftCancelMul } =
      { toAddSemigroup := toSemigroup_1, toZero := toOne_1, zero_add := one_mul_1, add_zero := mul_one_1,
        nsmul := npow_1, nsmul_zero := npow_zero_1, nsmul_succ := npow_succ_1, add_comm := mul_comm_1,
        toIsLeftCancelAdd := toIsLeftCancelMul_1 }