let x1, x2, p1, p2 be Nat; :: thesis: ( ((2 * x1) + 1) / (2 |^ p1) = x2 / (2 |^ p2) implies p1 <= p2 )
assume A1: ((2 * x1) + 1) / (2 |^ p1) = x2 / (2 |^ p2) ; :: thesis: p1 <= p2
assume p2 < p1 ; :: thesis: contradiction
then p2 + 1 <= p1 by NAT_1:13;
then reconsider P = p1 - (p2 + 1) as Nat by NAT_1:21;
p1 = P + (p2 + 1) ;
then ( 2 |^ p1 = (2 |^ P) * (2 |^ (p2 + 1)) & 2 |^ (p2 + 1) = 2 * (2 |^ p2) ) by NEWTON:6, NEWTON:8;
then ( ((2 * x1) + 1) * (2 |^ p2) = x2 * ((2 |^ P) * (2 * (2 |^ p2))) & x2 * ((2 |^ P) * (2 * (2 |^ p2))) = ((x2 * (2 |^ P)) * 2) * (2 |^ p2) ) by A1, XCMPLX_1:95;
hence contradiction by XCMPLX_1:5; :: thesis: verum