proposition: Lemma cleT_ell a b: cardinalp a -> cardinalp b -> [\/ a = b, a <c b | b <c a].
proof: Proof. move=> ca cb. move: (ca)(cb) => [oa _] [ob _]. case: (ordinal_inA oa ob) => h. - by constructor 2; move: (ordinal_sub2 ob h) => [p1 p2]. - by constructor 3; move: (ordinal_sub2 oa h) => [p1 p2]. - by constructor 1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)