match p with
| 0 =>
  apply False.elim
  apply Nat.not_lt_zero 1
  assumption
| Nat.succ 0 =>
  apply False.elim
  apply Nat.lt_irrefl 1
  assumption
| q+2 =>
  rw [nat_val_succ, Nat.mod_self, if_neg _]
  rw [Nat.div_self, nat_val_succ, if_pos, zero_add]
  rw [Nat.mod_eq_of_lt]
  exact Nat.succ_ne_zero 0
  assumption
  exact lt_trans (Nat.lt_succ_self 0) gt1
  exact Ne.irrefl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
⊢ nat_valuation p p = 1
no goals