p n : ℕ
hp : 1 ≤ padicValNat p n
h : ¬p ∣ n
⊢ False
p n : ℕ
hp : 1 ≤ padicValNat p n
⊢ p ∣ n
by_contra h
p n : ℕ
hp : 1 ≤ 0
h : ¬p ∣ n
⊢ False
p n : ℕ
hp : 1 ≤ padicValNat p n
h : ¬p ∣ n
⊢ False
rw [padicValNat.eq_zero_of_not_dvd h] at hp
no goals
p n : ℕ
hp : 1 ≤ 0
h : ¬p ∣ n
⊢ False
exact lt_irrefl 0 (lt_of_lt_of_le zero_lt_one hp)