Abstract real normalization of the material gradient PDE estimate.

theorem AVenhance.Infra.Section4.amnr_material_gradient_rate_le {κ S H G K Cb Ccoeff Cd D W : ℝ} (hK : 0 ≤ K) (hG : 0 ≤ G) (hC : 0 ≤ Ccoeff) (_hCd : 0 ≤ Cd) (hD : 0 ≤ D) (hW : 0 ≤ W) (hH : 0 ≤ H) (hRate : κ * S ^ 2 ≤ Cd * H) : ((2 * κ * K * G + 2 * K * (D * (Ccoeff * κ) * G)) * S ^ 2 + D * Cb * H * G) * W ≤ (1 + 2 * Cd * K * (1 + D * Ccoeff) + D * Cb) * G * (W * H)