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