proposition: Lemma CS_sup E: cardinal_set E -> cardinalp (\csup E).
proof: Proof. move=> alc. have os: ordinal_set E by move=> t /alc/proj1. have oe:= (OS_sup os). apply /cardinalP; split => // z zE /card_eqP ezE. move/setU_P:zE => [a za ax]. move/cardinalP: (alc _ ax) =>[_ h]; case: (h _ za). apply/card_eqP; apply:cleA. - by move: (sub_smaller (setU_s1 ax)); rewrite ezE. - exact (sub_smaller (ordinal_transitive (os _ ax) za)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)