no goals
𝓕 : Type ?u.1115291
𝕜 : Type ?u.1115294
α : Type u_1
ι : Type ?u.1115300
κ : Type ?u.1115303
E : Type ?u.1115306
F : Type ?u.1115309
G : Type ?u.1115312
inst✝² : SeminormedCommGroup E
inst✝¹ : SeminormedCommGroup F
a✝ a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
inst✝ : SeminormedCommGroup α
n : ℤ
a : α
⊢ ‖a ^ n‖ ≤ ‖n‖ * ‖a‖
rcases n.eq_nat_or_neg with ⟨n, rfl | rfl⟩ <;> simpa using norm_pow_le_mul_norm n a