apply Nat.ne_of_gt
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q m : ℕ
hq : 1 < q + 2
hmq : (m + 1) % (q + 2) = 0
⊢ (m + 1) / (q + 2) ≠ 0
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q m : ℕ
hq : 1 < q + 2
hmq : (m + 1) % (q + 2) = 0
⊢ 0 < (m + 1) / (q + 2)