no goals
𝕜 : Type u_1
B : Type ?u.298327
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
⊢ Nat.card ↑{u | addOrderOf u = n} ≠ 0
simpa only [coe_setOf, card_addOrderOf_eq_totient p] using (Nat.totient_pos hn).ne'