rw [Nat.mod_eq_of_lt]
case hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ (0 + 1) % (q + 2) ≠ 0

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ 0 < q + 1 + 1

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ ¬0 ≠ 0
case hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ 0 + 1 ≠ 0

case hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ 0 + 1 < q + 2

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ 0 < q + 1 + 1

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ ¬0 ≠ 0