proposition: Lemma cofinality_card x: infinite_c x -> cofinality_c x = cofinality x.
proof: Proof. move=> icx. move: (icx) => [cx _]; move: (cx)=> [ox _]. move: (CS_cofinality ox) (cofinality_pr3 ox) => ca cb. move: (cofinality_c_rw (infinite_ge2 icx)) => [p3 p4 p5]. apply: oleA. move: (OS_cofinality ox) => sa; apply: p5 => //. move:(cofinality_pr4 ox) => [f [[[ff sf tf] cff] _] _]. set g := Lg (\cf x) (fun z => cardinal (Vf f z)). have pa: csum_of_small1 x g. rewrite /g; split; fprops; hnf; aw => t tsf; rewrite LgV//. have pa: Vf f t <o x by apply /(oltP ox); rewrite - tf; Wtac. apply/ocle2P => //; exact: (proj31_1 pa). have pb: domain g = \cf x by rewrite /g; aw. have pc: \cf x <=c x by apply:ocle3. exists g; split => //; apply: cleA. move: (cprod_inf1 pc icx)(csum_of_small_b2 pa);rewrite pb. move => ca' cb'; exact:(cleT cb' ca'). set f1 := Lg (\cf x) (Vf f). have <-: cardinal (unionb f1) = x. rewrite - (card_card cx); congr cardinal; rewrite /f1;set_extens t. move /setUb_P;aw;move =>[y ydf]; rewrite LgV// => tv. have pd: inc (Vf f y) x by rewrite - tf; Wtac. exact (ordinal_transitive ox pd tv). move: (infinite_card_limit2 icx) => [_ _ lx]. move /lx /cff => [z za /oleSltP zb]; apply/setUb_P; aw; ex_tac. by rewrite LgV//; move/ oltP0: zb => [_ _]. have <-: csumb (domain f1) (fun a => cardinal (Vg f1 a)) = csum g. rewrite /csumb/f1/g; aw; congr csum; apply:Lg_exten. by move => t tdf /=; rewrite !LgV. by move: (csum_pr1 f1). move: p4 => [f [[qa qb] df q3]]; move: (p3) => [[ocfx _ _] _]. set T := fun_image (domain f) (Vg f). have Ts: forall a, inc a T -> a <=c x. by move => t /funI_P [z zd ->]; move: (qb _ zd) => []. have cst:cardinal_set T by move => t tt; exact: (proj31(Ts _ tt)). set s := union T. have sx: s <=c x by apply: card_ub_sup. case: (equal_or_not s x) => esx. move: (cofinality_rw ox) => [pa pb]; apply => //. have ta: lf_axiom (Vg f) (cofinality_c x) x. move=> t; rewrite - df => tdf; apply /(oltP ox). apply: oclt; exact:(qb _ tdf). set g:= Lf (Vg f) (cofinality_c x) x. exists g; split. rewrite /g; hnf; saw; apply: lf_function => //. have osT:ordinal_set T by move => t /cst h; apply: OS_cardinal. move => t /(oltP ox); rewrite - esx => tx. move: (olt_sup osT tx) => [z /funI_P [w]]. by rewrite df esx; move => u1 u2 [u3 _]; ex_tac; rewrite /g LfV// - u2. have le1:x <=c s *c cofinality_c x. rewrite - csum_of_same -df -q3; apply: csum_increasing; aw; trivial. move=> a adf; rewrite LgV//; apply: card_sup_ub => //; apply /funI_P; ex_tac. suff: (cofinality_c x *c s) <=c cofinality_c x. by rewrite cprodC; move=> le2; rewrite (cleA p3 (cleT le1 le2)). move:(CS_sup cst) (proj31 p3)=> cs cy. case: (finite_or_infinite cs) => fs. case: (finite_or_infinite cy) => fy. have fp: finite_c (s *c cofinality_c x). by apply /NatP; apply: NS_prod; apply /NatP. case: (cleNgt le1 (clt_fin_inf fp icx)). exact: (cprod_inf2 fs fy). have lt1: (s *c cofinality_c x) <=c s -> False. by move => le2; move: (cleA sx (cleT le1 le2)) => bad; case: esx. case: (finite_or_infinite cy) => fy; first by case:(lt1 (cprod_inf2 fy fs)). case: (cleT_ee cs cy) => le3; first exact:(cprod_inf1 le3 fy). case: (lt1 (cprod_inf1 le3 fs)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)