proposition: Lemma cofinality_c_pr2 x: \2c <=c x -> exists f, [/\ csum_of_small1 x f, domain f = (cofinality_c x), csum f = x & (allf f (fun z => z <> \0c)) ].
proof: Proof. move=> h; move: (cofinality_c_rw h) => [pa pb pc]. move: pb => [f [[pd pe] pf pg]]. set j := Zo (domain f) (fun z => Vg f z <> \0c). have sj: sub j (domain f) by apply: Zo_S. have qa: (forall i, inc i ((domain f) -s j) -> Vg f i = \0c). move=> i /setC_P [r1] /Zo_P r2; ex_middle h0; case: r2; split => //. move: (csum_zero_unit sj qa) => h1; rewrite h1 in pg. have h2: csum_of_small1 x (Lg j (Vg f)). split; [ fprops | by hnf; aw;move=> a ad; rewrite LgV//;apply: pe; apply: sj]. move: (csum_commutative1 h2) => [g []]; aw => ga gb gc gd. have xsg: csum g = x by rewrite - gc. set z := (cardinal j). have oz: ordinalp z by apply: OS_cardinal; apply: CS_cardinal. have h3: cofinality_c_ex x z by exists g. move: (pc _ oz h3) => le2. have le3: z <=c cofinality_c x. move : (sub_smaller sj); rewrite pf -/z card_card //; exact: (proj31 pa). rewrite (oleA le2 (ocle le3)). exists g; split => // i idg bad. have : inc \0c (range (Lg j (Vg f))). rewrite - gd;apply/(range_gP (proj1 ga)); ex_tac. rewrite Lg_range => /funI_P [u uj]. by move: uj => /Zo_hi pdd pw; case: pdd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)