proposition: Lemma cnext_sup F: cardinal F <=c C -> sub F E -> inc (\osup F) E.
proof: Proof. move: (iC) => [cc _]pa pb; apply/(cnextP cc); split. by apply: OS_sup => t/pb /cnextP []. rewrite - setUb_identity. move: (csum_pr1 (identity_g F)); rewrite identity_d /csumb;set f := Lg _ _. have cdf: cardinal (domain f) <=c C by rewrite /f; aw. have etc: forall i, inc i (domain f) -> Vg f i <=c C. rewrite /f; aw; move => i idf. rewrite LgV // identity_ev //. by move /cnextP: (pb _ idf) => []. move: (notbig_family_sum iC cdf etc) => ha hb; exact :cleT hb ha. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)