have ha : a % 2 = 1 := by
  have : a % 2 = 0 ∨ a % 2 = 1 := mod_two a
  simpa [show a % 2 ≠ 0 from by simpa [←mod_eq_zero_iff_dvd] using A.1] 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
⊢ 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
⊢ False