proposition: Lemma ord_cofinal_p4 A C (E:= cnext C): infinite_c C -> ord_cofinal A E -> cardinal A = E.
proof: Proof. move => sa [sb sc]. have [pa pb pc] := (cnext_pr1 (proj1 sa)). have ose:= (Os_ordinal (proj1 pa)). case: (cleT_el (CS_cardinal A) (proj1 sa)); last first. move /pc; move: (sub_smaller sb);rewrite (card_card pa);exact:cleA. move => cyc; move: (cnext_sup sa cyc sb)=> xsb. have sse:= (ord_sup_1cofinal (conj sb sc) ose). have hy:= (infinite_card_limit2( cle_inf_inf sa (proj1 pb))). have ue:=(limit_nonsucc hy). by move: (ordinal_irreflexive (proj1 pa)); rewrite {1} ue -[opred _] sse. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)