exact ⟨q, rfl, pow2_mul_two.mp H⟩
case pos.intro.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
q : M
H : Pow2 (2 * q)
hp : 1 < 2 * q
⊢ ∃ q_1, 2 * q = 2 * q_1 ∧ Pow2 q_1
no goals