p : ℕ
hp : Fact (Nat.Prime p)
⊢ (↑p)⁻¹ < 1
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ‖↑p‖ < 1
rw [norm_p]
case ha
p : ℕ
hp : Fact (Nat.Prime p)
⊢ 1 < ↑p
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (↑p)⁻¹ < 1
apply inv_lt_one
no goals
case ha
p : ℕ
hp : Fact (Nat.Prime p)
⊢ 1 < ↑p
exact_mod_cast hp.1.one_lt