proposition: Lemma cofinality_infinite x: infinite_c x -> infinite_c (cofinality_c x).
proof: Proof. move=> icx; move: (infinite_ge2 icx) => x1. move: (cofinality_c_rw x1) => [pc pd pe]. have cs:=proj31 pc. case: (finite_or_infinite cs) => // cf. move: (cf); rewrite - (card_card cs) -/(finite_set _) => fs. move: pd => [f [[fa fb] fc fd]]. set E := fun_image (domain f) (fun z => Vg f z). have fe: finite_set E by apply: finite_fun_image; ue. have nee: nonempty E. apply:funI_setne; apply/nonemptyP => dfe. case: (infinite_nz icx);rewrite - fd; exact: (csum_trivial dfe). have cse: cardinal_set E. move=> t /funI_P [z zdf ->]; exact: (proj31_1 (fb _ zdf)). move: (wordering_cle_pr cse) => [qa qb]. move: (finite_set_torder_greatest (worder_total qa)); rewrite qb => aux. move: (aux fe nee)=> [t []]; rewrite qb => qc qd. have tx: t <c x by move: qc => /funI_P [z0 /fb zd ->]. have tx1: (allf f (cardinal_le^~ t)). move=> i idf; have vE: inc (Vg f i) E by apply /funI_P; ex_tac. by move: (qd _ vE) => /graph_on_P1 [_ _]. move: (csum_of_small_b1 (conj fa tx1)); rewrite fc => sc. have ct:=proj31_1 tx. case: (finite_or_infinite ct) => // fct. have fp: finite_c (t *c cofinality_c x). by apply /NatP; apply: NS_prod; apply/NatP. by move: (clt_fin_inf fp icx); rewrite - {2} fd=> /(cleNgt sc). move: (clt_fin_inf cf fct) => [le1 _]. move: (cprod_inf1 le1 fct) => sb. by move: (cleT sc sb); rewrite fd => /(cltNge tx). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)