exact lt_of_le_of_lt (by simp) hjsi
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this✝¹ : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
psqi : Pow2 (√i)
one_lt_sqi : 1 < √i
j : M
hj : j ≤ m % (2 * √i)
pj : Pow2 j
lt2 : 2 < j
hjsi : j < 2 * √i
this✝ : LenBit j m ↔ (√j) ^ 2 = j ∧ LenBit (√j) m
hsqj : (√j) ^ 2 = j
this : Pow2 (√j)
⊢ √j < 2 * √i
no goals