proposition: Lemma cofinality_c_pr3 x: infinite_c x -> exists f, [/\ csum_of_small1 x f, domain f = (cofinality_c x), csum f = x & (allf f (fun z => \2c <=c z)) ].
proof: Proof. move => icx; move: (infinite_ge2 icx) => x1. move: (cofinality_c_rw x1) => [pa pb pc]. move: pb => [f [[pd1 pd2] pe pf]]. move: (sum_of_sums (Vg f) (fun _:Set => \2c) (domain f)). rewrite csum_of_same csum_gr pf pe. have ->: x +c \2c *c cofinality_c x = x. move: (csum_inf pa icx) => xx. by rewrite - csum_nn csumA xx xx. move=> xv. exists (Lg (cofinality_c x) (fun i => Vg f i +c \2c)); split. - split; [ fprops | hnf; aw => i idf; rewrite LgV//]. rewrite -pe in idf;move: (pd2 _ idf) => lt1. apply:csum_inf5 => //; apply: (clt_fin_inf finite_2 icx). - by aw. - done. - hnf; aw; move=> i ic; rewrite LgV//; apply: csum_Mle0; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)