let x1, x2, y1, y2, p1, p2 be Nat; :: thesis: ( x1 + (y1 / (2 |^ p1)) < x2 + (y2 / (2 |^ p2)) & y1 < 2 |^ p1 & y2 < 2 |^ p2 implies x1 <= x2 )
assume that
A1: ( x1 + (y1 / (2 |^ p1)) < x2 + (y2 / (2 |^ p2)) & y1 < 2 |^ p1 & y2 < 2 |^ p2 ) and
A2: x2 < x1 ; :: thesis: contradiction
A3: x2 + 1 <= x1 by A2, NAT_1:13;
( 0 <= y1 / (2 |^ p1) & y2 / (2 |^ p2) < 1 ) by A1, XREAL_1:189;
then A4: ( x1 + 0 <= x1 + (y1 / (2 |^ p1)) & x2 + (y2 / (2 |^ p2)) < x2 + 1 ) by XREAL_1:6;
then x2 + (y2 / (2 |^ p2)) < x1 by A3, XXREAL_0:2;
hence contradiction by A4, A1, XXREAL_0:2; :: thesis: verum