exact False.elim <| not_le.mpr (ppi.two_lt ne2) hi
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
hi : i ≤ 2
ne2 : ¬i = 2
ppi : PPow2 i
⊢ Seqₛ.Even 4 (2 * 4) i ∨ Seqₛ.Odd 4 (2 * 4) i
no goals