linarith only [this]
case inr.inl
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            b ≤ a →
              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
Hba : ¬b ≤ a
h4 : a ≤ b
hca : c ≤ a
this : b ^ 2 * a + b ^ 2 * c + a ^ 2 * b + a ^ 2 * c + c ^ 2 * b + c ^ 2 * a ≤ b ^ 3 + a ^ 3 + c ^ 3 + 3 * b * a * 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