linarith [h1 a c b ha hc hb h3]
case inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
h1 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
              a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hcb : ¬c ≤ b
h3 : b ≤ c
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
no goals