Exact-threshold scalar contradiction

This is the final scalar step for the exact 9/10 cut argument.

theorem LeanPool.DrossFractionalTriangleDecomposition.dross_3_4_to_false_exact (n m k cc wΔ T_A T_B δ : ℝ) (hδ0 : 0 < δ) (hδ1 : δ ≤ 1 / 10) (hcc : 0 < cc) (hccrel : 2 * wΔ = cc * (3 * n * (1 - δ) - 3)) (hn : 20 ≤ n) (hTA1 : (1 - 2 * δ) * n ≤ T_A) (hTA2 : T_A ≤ n) (hTB1 : (1 - 2 * δ) * n ≤ T_B) (mbound : 2 * m ≤ (1 - δ + 2 * δ ^ 2) * n ^ 2 + 4 + n - 6 * δ * n) (ineq3 : cc * (T_A * (T_A - δ * n) / 2 - k) < T_A * wΔ - 1) (ineq4 : cc * (T_B * (T_B - δ * n) / 2 - (m - k)) < 1 - T_B * wΔ) : False