proposition: Lemma cleT_el a b: cardinalp a -> cardinalp b -> a <=c b \/ b <c a.
proof: Proof. move=> ca cb; case: (cleT_ell ca cb). + move=> ->; left; fprops. + by move => [p1 _]; left. + by right. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)