theorem zltnle (a b: nat): $ a ~b <=Z a $;
(b <=Z a <-> ~a <Z b) -> (a <Z b <-> ~b <=Z a)
b <=Z a <-> ~a <Z b
a <Z b <-> ~b <=Z a