proposition: Lemma ord_cofinal_p5 A C (E:= cnext C): infinite_c C -> ord_cofinal A E -> ordinal (ole_on A) = E.
proof: Proof. move => pa pc; move: (proj1 pc) => pb. have ca:= (ord_cofinal_p4 pa pc). set x := ordinal (ole_on A). have [sa sb sc] := (cnext_pr1 (proj1 pa)). have osa:=(Os_sub (Os_ordinal (proj1 sa)) pb). have [pe pf]:=(wordering_ole_pr osa). move: (cardinal_of_ordinal pe); rewrite pf -/x ca => cc. have [oe hh] : cardinalp E by exact: (proj32_1 sb). have ox: ordinalp x by apply: OS_ordinal. have cc2: E \Eq x by apply /card_eqP; symmetry; rewrite cc -/E card_card. apply: oleA; last by split => //;exact: (hh _ ox cc2). apply/ordinal_le_P0; split=> //. move: (the_ordinal_iso1 pe); rewrite -/x. have o1 :=(proj1 (ordinal_o_wor oe)). have o2 := (proj1 pe). have o3:order (ordinal_o x) by fprops. set f := (the_ordinal_iso _) => ff. rewrite /order_le; split => //; rewrite ordinal_o_sr; exists f, A; split => //. have -> //: (induced_order (ordinal_o E) A = (ole_on A)). have aso :sub A (substrate (ordinal_o E)) by rewrite ordinal_o_sr. have [sd se]:= (iorder_osr o1 aso). apply: order_exten => // u v; split. move /iorder_gleP => [ua va /ordo_leP [_ _ ha]]; apply /graph_on_P1. split => //; split => //; fprops. move => /graph_on_P1[ua ub [_ _ uv]]; apply /iorder_gleP; split => //. apply/ordo_leP;split => //; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)