proposition: Lemma zleT_ell a b: intp a -> intp b -> [\/ a = b, a <z b | b <z a].
proof: Proof. move => pa pb; case: (equal_or_not a b); first by constructor 1. by move => na; case: (zleT_ee pa pb)=> h1; [constructor 2 | constructor 3]; split => //; apply: nesym. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)