{α : Type u_5} →
  {motive : NonUnitalSeminormedRing α → Sort u} →
    ([toNorm : Norm α] →
        [toNonUnitalRing : NonUnitalRing α] →
          [toPseudoMetricSpace : PseudoMetricSpace α] →
            (dist_eq : ∀ (x y : α), dist x y = ‖-x + y‖) →
              (norm_mul_le : ∀ (a b : α), ‖a * b‖ ≤ ‖a‖ * ‖b‖) →
                motive
                  { toNorm := toNorm, toNonUnitalRing := toNonUnitalRing, toPseudoMetricSpace := toPseudoMetricSpace,
                    dist_eq := dist_eq, norm_mul_le := norm_mul_le }) →
      (t : NonUnitalSeminormedRing α) → motive t