proposition: Lemma cofinality_c_rw x (y:= cofinality_c x): \2c <=c x -> [/\ y <=c x, cofinality_c_ex x y & (forall z, ordinalp z -> (cofinality_c_ex x z) -> y <=o z)].
proof: Proof. move=> x2. have cx:= proj32 x2. move: (cx) => [ox _]. have x1:=(clt_leT clt_12 x2). pose p := cofinality_c_ex x. have px: p x. exists (cst_graph x \1c); split. - split;[ fprops | hnf; aw=> a ax; rewrite LgV//]. - by aw. - by rewrite [csum _](csum_of_ones x); apply: card_card. move: (least_ordinal1 ox px) => []. rewrite -/(cofinality_c x) -/y; move=> oy py pb. have pa: forall z, ordinalp z -> p z -> y <=o z. by move => z oz pz; move: (pb _ oz pz)=> yz. split => //. move: py => [f [qa qb qc]]. move: (csum_commutative1 qa)=> [g [ga gb gc gd]]. have pcy: p (cardinal y) by exists g; rewrite gb qb - gc qc. move: (oleA (pa _ (proj1 (CS_cardinal y)) pcy) (card_ord_le oy)) => H. split => //; [ rewrite H; fprops | exact: (pb _ ox px)]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)