have : a * b % 2 = 1 := by simp [mod_mul, ha, hb]
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
ha : a % 2 = 1
hb : b % 2 = 1
⊢ False
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
ha : a % 2 = 1
hb : b % 2 = 1
this : a * b % 2 = 1
⊢ False