p : ℕ
hp : 1 < p
neq_one : ¬p = 1 ↔ True
⊢ padicValNat p p = 1
p : ℕ
hp : 1 < p
⊢ padicValNat p p = 1
have neq_one : ¬p = 1 ↔ True := iff_of_true hp.ne' trivial
p : ℕ
hp : 1 < p
neq_one : ¬p = 1 ↔ True
eq_zero_false : p = 0 ↔ False
⊢ padicValNat p p = 1
p : ℕ
hp : 1 < p
neq_one : ¬p = 1 ↔ True
⊢ padicValNat p p = 1
have eq_zero_false : p = 0 ↔ False := iff_false_intro (zero_lt_one.trans hp).ne'
no goals
p : ℕ
hp : 1 < p
neq_one : ¬p = 1 ↔ True
eq_zero_false : p = 0 ↔ False
⊢ padicValNat p p = 1
simp [padicValNat, neq_one, eq_zero_false]