theorem Th26: :: SURREALN:26

for n, m, p being Nat st (2 * m) + 1 < 2 |^ p holds
born (uDyadic . (n + (((2 * m) + 1) / (2 |^ p)))) = (n + p) + 1