theorem Th31: :: STIRL2_1:31

for n being Nat st n <> 0 holds
n block 0 = 0