theorem Th34: :: SURREALN:34
for x1, x2, p1, p2 being Nat st ((2 * x1) + 1) / (2 |^ p1) = x2 / (2 |^ p2) holds
p1 <= p2