intro H
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
m : ℕ
hm : 0 < m
hmq : m % q ≠ 0
⊢ ¬(m % q == 0) = true
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
m : ℕ
hm : 0 < m
hmq : m % q ≠ 0
H : (m % q == 0) = true
⊢ False