{M : Type u} →
  {motive : AddMonoid M → Sort u_1} →
    (t : AddMonoid M) →
      ([toAddSemigroup : AddSemigroup M] →
          [toZero : Zero M] →
            (zero_add : ∀ (a : M), 0 + a = a) →
              (add_zero : ∀ (a : M), a + 0 = a) →
                (nsmul : ℕ → M → M) →
                  (nsmul_zero : ∀ (x : M), nsmul 0 x = 0) →
                    (nsmul_succ : ∀ (n : ℕ) (x : M), nsmul (n + 1) x = nsmul n x + x) →
                      motive
                        { toAddSemigroup := toAddSemigroup, toZero := toZero, zero_add := zero_add,
                          add_zero := add_zero, nsmul := nsmul, nsmul_zero := nsmul_zero, nsmul_succ := nsmul_succ }) →
        motive t