no goals
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : f ≈ 0
⊢ 0 ≤ norm f
simp [hf, norm]
no goals
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
⊢ 0 ≤ norm f
simp [norm, hf, padicNorm.nonneg]