theorem zlt01 (a: nat): $ a odd a $;
a -Z 0 = a -> (odd (a -Z 0) <-> odd a)
a -Z 0 = a -> (a <Z 0 <-> odd a)
a -Z 0 = a
a <Z 0 <-> odd a