theorem zltle (a b: nat): $ a a <=Z b $;
a <Z b <-> ~b <=Z a
b <=Z a \/ a <=Z b
~b <=Z a -> a <=Z b
a <Z b -> a <=Z b