simp at this
case intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
p : M
pp : Pow2 p
q : M
hq : q ≤ p
H : Exponential (log p) q
hp : p < 2 * q
ne : ¬p = q
this✝ : q < p
this : 2 * q < 2 * q
⊢ False
no goals