suffices H : 0 ≤ (a - b)^2 by linarith
case mk.mk
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
h1 : 0 < b * a
⊢ 2 * (b * a) ≤ a * a + b * b
case mk.mk
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
h1 : 0 < b * a
⊢ 0 ≤ (a - b) ^ 2