proposition: Lemma card_ub_sup E y: cardinalp y -> (forall i, inc i E -> i <=c y) -> \csup E <=c y.
proof: Proof. move => cy ali. have csE: cardinal_set E by move => i /ali []. have: (\csup E) <=o y by apply: (ord_ub_sup (proj1 cy)) => o /ali/ocle. by move /ocle1; rewrite (card_card (CS_sup csE)) (card_card cy). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)