suffices H : 2 * (b * a) ≤ a * a + b * b by exact (le_div_iff h1).mpr H
case mk.mk
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
h1 : 0 < b * a
⊢ 2 ≤ (a * a + b * b) / (b * a)
case mk.mk
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
h1 : 0 < b * a
⊢ 2 * (b * a) ≤ a * a + b * b