proposition: Lemma cofinality_c_finite x: \2c <=c x -> finite_c x -> cofinality_c x = \2c.
proof: Proof. move=> x1 fcx. move: (cofinality_c_rw x1) => [p3 p4 p5]. set y:= cofinality_c x. have xnz :=(proj2 (clt_leT (clt_02) x1)). move: p4 => [f [[q1 q2] df q3]]. case: (ord2_trichotomy (proj1 (proj31 p3))) => h. have dfe: domain f = emptyset by rewrite df h. by case: xnz; rewrite -q3 (csum_trivial dfe). have df1: domain f = singleton \0c by rewrite df h. have zc: inc \0c (domain f) by rewrite df1; fprops. move: (q2 _ zc); rewrite -q3 (csum_trivial1 df1). move =>[le1]. by rewrite (card_card (proj31 le1)). apply: (oleA) => //; apply: p5; first by apply: OS2. have xB: natp x by apply /NatP. move: (cpred_pr xB (nesym xnz)) => []; set p:= cpred x; move => p4 p5. have lpx: p <c x by rewrite p5; apply: cltS. have cp:= (proj31_1 lpx). move: (esym p5); rewrite (csucc_pr4 cp). rewrite (csum2_pr (doubleton_fam_variant p \1c C1_ne_C0)). set g:= (variantL _ _ _ _) => p7. have dg : \2c = domain g by rewrite /g/variantL; aw. have p6: forall i, inc i (domain g) -> Vg g i <c x. have aux:= (clt_leT clt_12 x1). by move => i; rewrite /g {1} /variantL; aw; case /set2_P => ->; aw. exists g;split => //; split => //; rewrite /g/variantL; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)