have hb : b % 2 = 1 := by
  have : b % 2 = 0 ∨ b % 2 = 1 :=
    le_one_iff_eq_zero_or_one.mp <| lt_two_iff_le_one.mp <| mod_lt b (b := 2) (by simp)
  simpa [show b % 2 ≠ 0 from by simpa [←mod_eq_zero_iff_dvd] using A.2] using this
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
⊢ 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
⊢ False