theorem :: EUCLID:4

for n being Nat holds abs (0* n) = n |-> 0