for n being Nat holds
( n block 0 = 1 iff n = 0 )