{α : Type u_1} →
  {motive : NonAssocRing α → Sort u} →
    ([toNonUnitalNonAssocRing : NonUnitalNonAssocRing α] →
        [toOne : One α] →
          (one_mul : ∀ (a : α), 1 * a = a) →
            (mul_one : ∀ (a : α), a * 1 = a) →
              [toNatCast : NatCast α] →
                (natCast_zero : ↑0 = 0) →
                  (natCast_succ : ∀ (n : ℕ), ↑(n + 1) = ↑n + 1) →
                    [toIntCast : IntCast α] →
                      (intCast_ofNat : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n) →
                        (intCast_negSucc : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)) →
                          motive
                            { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing, toOne := toOne, one_mul := one_mul,
                              mul_one := mul_one, toNatCast := toNatCast, natCast_zero := natCast_zero,
                              natCast_succ := natCast_succ, toIntCast := toIntCast, intCast_ofNat := intCast_ofNat,
                              intCast_negSucc := intCast_negSucc }) →
      (t : NonAssocRing α) → motive t