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