theorem NNReal.add_sub_two_mul_min_eq_max (s t : NNReal) : s + t - 2 * min s t = max (s - t) (t - s)