let a, b be ExtInt; :: thesis: ( a <= b implies 0 <= b - a )
assume a <= b ; :: thesis: 0 <= b - a
then a + (- a) <= b + (- a) by XXREAL_3:36;
hence 0 <= b - a by XXREAL_3:7; :: thesis: verum