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