theorem Th1: :: PDIFF_7:1

for i, j being Nat st i <= j holds
(0* j) | i = 0* i