proposition: Lemma card_sup_ub E: cardinal_set E -> forall i, inc i E -> i <=c \csup E.
proof: Proof. move => h; move: (CS_sup h) => cs. have os:= oset_cset h. move=> i ie; move: (ord_sup_ub os ie)=> [pa pb pc]; split; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)