no goals
α : Type u_1
β : Type ?u.12527
γ : Type ?u.12530
ι : Type ?u.12533
inst✝ : NonUnitalSeminormedRing α
a b : α
⊢ ‖a * b‖₊ ≤ ‖a‖₊ * ‖b‖₊
simpa only [← norm_toNNReal, ← Real.toNNReal_mul (norm_nonneg _)] using
  Real.toNNReal_mono (norm_mul_le _ _)