no goals
α : Type u_1
β : Type ?u.126931
γ : Type ?u.126934
ι : Type ?u.126937
inst✝ : SeminormedRing α
a : α
x✝ : 0 < 1
⊢ ‖a ^ 1‖₊ ≤ ‖a‖₊ ^ 1
simp only [pow_one, le_rfl]
no goals
α : Type u_1
β : Type ?u.126931
γ : Type ?u.126934
ι : Type ?u.126937
inst✝ : SeminormedRing α
a : α
n : ℕ
x✝ : 0 < n + 2
⊢ ‖a ^ (n + 2)‖₊ ≤ ‖a‖₊ ^ (n + 2)
simpa only [pow_succ _ (n + 1)] using
  le_trans (nnnorm_mul_le _ _) (mul_le_mul_left' (nnnorm_pow_le' a n.succ_pos) _)