apply hab
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b p : ℕ
hab : a * b % p ≠ 0
ha : a % p = 0
⊢ False
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b p : ℕ
hab : a * b % p ≠ 0
ha : a % p = 0
⊢ a * b % p = 0