enrich
nat
with
functions
sgn : nat → nat;
variables
m : nat;
n : nat;
axioms
sgn-0: sgn(0) = 0;
used for: s, ls;
sgn-s: n ≠ 0 → sgn(n) = 1;
used for: s, ls;
end enrich