proposition: Lemma regular_sup X b: regular_cardinal b -> cardinal X <c b -> (forall i, inc i X -> i <c b) -> \csup X <c b.
proof: Proof. move => ha hb hc. have ic := proj1 ha. set f := Lg X id. have ra:csum_of_small1 b f. by rewrite /f;split; fprops; hnf;aw; move => i ix; rewrite LgV//; apply: hc. have cd: cardinal (domain f) <c b by rewrite /f; aw. move /(infinite_regularP ic): ha => rb; move: (rb _ ra cd); apply: (cle_ltT). have CX: cardinal_set X by move => i /hc [[]]. move: (csum_pr1 f). have ->: csumb (domain f) (fun a => cardinal (Vg f a)) = csum f. rewrite /f /csumb Lgd;apply:csumb_exten => i idx /=; rewrite LgV//. exact:(card_card (CX _ idx)). by rewrite setUb_identity (card_card (CS_sup CX)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)