exact H.dvd (show r ≤ 2 * a from le_trans hr (le_mul_of_one_le_left (by simp) one_le_two)) ltr (Dvd.dvd.mul_left dvd 2)
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a : M
H : Pow2 (2 * a)
r : M
hr : r ≤ a
ltr : 1 < r
dvd : r ∣ a
⊢ 2 ∣ r
no goals