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