proposition: Lemma zle_ltT a b c: a <=z b -> b <z c -> a <z c.
proof: Proof. move => pa [pb pc];split; first apply: (zleT pa pb). move => ac; case: pc;apply :zleA => //; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)