theorem euled_f (a b c : ℝ) (h₀ : 0 < a ∧ 0 < b ∧ 0 < c) (h₁ : c < a + b) (h₂ : b < a + c) (h₃ : a < b + c) : 0 ≤ (a - b)^2 * (a + b - c) + (b - c)^2 * (b + c - a) + (c - a)^2 * (c + a - b) := by
  have h4 : 0 ≤ a + b - c := by linarith
  have h5 : 0 ≤ b + c - a := by linarith
  have h6 : 0 ≤ c + a - b := by linarith
  have e1 := mul_nonneg (sq_nonneg (a - b)) h4
  have e2 := mul_nonneg (sq_nonneg (b - c)) h5
  have e3 := mul_nonneg (sq_nonneg (c - a)) h6
  nlinarith [e1, e2, e3]

theorem euled_c (a b c : ℝ) (h₀ : 0 < a ∧ 0 < b ∧ 0 < c) (h₁ : c < a + b) (h₂ : b < a + c) (h₃ : a < b + c) (hq : 0 ≤ (a - b)^2 * (a + b - c) + (b - c)^2 * (b + c - a) + (c - a)^2 * (c + a - b)) : 0 ≤ (a - b)^2 * (a + b - c) + (b - c)^2 * (b + c - a) + (c - a)^2 * (c + a - b) := by
  exact hq

theorem euled_b0 (a b c : ℝ) (h₀ : 0 < a ∧ 0 < b ∧ 0 < c) (h₁ : c < a + b) (h₂ : b < a + c) (h₃ : a < b + c) (h : 0 ≤ (a - b)^2 * (a + b - c) + (b - c)^2 * (b + c - a) + (c - a)^2 * (c + a - b)) : 0 ≤ a^2 * b * (a - b) + b^2 * c * (b - c) + c^2 * a * (c - a) := by
  have e1 : 0 < a + b - c := by linarith
  have e2 : 0 < b + c - a := by linarith
  have e3 : 0 < c + a - b := by linarith
  nlinarith [mul_nonneg (sq_nonneg (a - b)) e1.le, mul_nonneg (sq_nonneg (b - c)) e2.le, mul_nonneg (sq_nonneg (c - a)) e3.le]

theorem imo_1983_p6 (a b c : ℝ) (h₀ : 0 < a ∧ 0 < b ∧ 0 < c) (h₁ : c < a + b) (h₂ : b < a + c) (h₃ : a < b + c) : 0 ≤ a^2 * b * (a - b) + b^2 * c * (b - c) + c^2 * a * (c - a) := by
  exact euled_b0 a b c h₀ h₁ h₂ h₃ (euled_c a b c h₀ h₁ h₂ h₃ (euled_f a b c h₀ h₁ h₂ h₃))