proposition: Lemma card_LS_res X P : cardinal (LS_res X P) <=c cardinal P +c aleph0.
proof: Proof. rewrite /LS_res. move:(induction_defined_pr (LS_nextP X) P). rewrite -/LS_res; move => [h1 h2 h3 h4]. have ff:= proj1 h2. rewrite - (surjective_pr0 h2) (ImfE ff) -(setUb_alt(function_fgraph ff)). move: (csum_pr1 (graph (induction_defined (LS_nextP X) P))). rewrite (domain_fg (proj1 h2)) h1; rewrite /csumb. set g := Lg Nat _ => h6. move: (aleph0_pr P) => /=; set c1 := cardinal P +c aleph0. move => [k1 k2 k3 k4 [k5 k6 k7 k8]]. have k9: cardinal (domain g) <=c c1 by rewrite /g; aw; rewrite - k1. have hc:= CIS_aleph0. have k10:(forall i, inc i (domain g) -> Vg g i <=c c1). rewrite /g;aw => i iN; rewrite LgV//; rewrite -/(Vf _ _); move: i iN. apply: Nat_induction; first by rewrite h3. move => n nN; rewrite (h4 _ nN); set P1 := Vf _ _ => Hrec. move:(card_LS_nextP X P1) => h7. move: (csum_Mleeq aleph0 Hrec); rewrite /c1 - csumA csum_inf1 // => ha. exact: (cleT h7 ha). by apply: cleT (notbig_family_sum k5 k9 k10). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)