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