have h12 : 0 ≤ (c - a) * (c - b) := by nlinarith only [Hba, Hcb]
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
h6 : 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c)
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
h6 : 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c)
h12 : 0 ≤ (c - a) * (c - b)
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)