ring
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ (a ^ 4 + b ^ 4 + c ^ 4) ^ 2 - a ^ 2 * ((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3) =
    2 * (a ^ 2 * (b ^ 2 - c ^ 2)) ^ 2 + (b ^ 4 - c ^ 4) ^ 2 + (2 * (a ^ 2 * b * c - b ^ 2 * c ^ 2)) ^ 2
no goals