have : 0 ≤ (s - t) ^ 2 * ((s + 7 * t) ^ 2 + 2 * (4 * t) ^ 2) := by positivity
s t : ℝ
⊢ s * t ^ 3 * 4 ^ 4 ≤ (3 * t + s) ^ 4
s t : ℝ
this : 0 ≤ (s - t) ^ 2 * ((s + 7 * t) ^ 2 + 2 * (4 * t) ^ 2)
⊢ s * t ^ 3 * 4 ^ 4 ≤ (3 * t + s) ^ 4