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

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