simpa [Seqₛ.Odd, ext_rem, ppj, ppj.sq, ppi, *] using H
case inr.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y y' X Y i : M
h : Seqₛ y X Y
ppi : PPow2 i
hi : y' ^ 2 < i
hy : y' ≤ y
j : M
hj : j ≤ y'
ne2 : j ≠ 2
ppj : PPow2 j
this✝ : j ^ 2 < i
this : j < i
H : Odd X Y j
⊢ Odd (X % i) (Y % i) j
no goals