a - (min (a,b)) >= (min (a,b)) - (min (a,b)) by XREAL_1:9, XXREAL_0:17;
hence not a - (min (a,b)) is negative ; :: thesis: verum