proposition: Lemma cofinality_sd a: ordinalp a -> (cofinality a) = (cofinality_alt a).
proof: Proof. move => oa. move: (ordinal_o_wor oa) => woa; move: (woa) => [ora _]. have ofa: ordinalp (cofinality_alt a). move: (cofinality'_pr0 woa) => [pa pb]. exact: (pb _ (ordinal_setI pa pb)). have ocfa: ordinalp (cofinality a) by apply: OS_cofinality. apply: oleA. move: (cofinality_pr1 oa) => [z [za cfz woz xx]]. move: cfz => [pb pc]. move: (cofinality_rw oa) => [pa _ h] => //. suff cex: cofinal_function_ex a (cofinality_alt a) by exact: (h _ ofa cex). move: (orderIS (ordinal_o_is woz)); rewrite -xx. move => [f isf]. move: (isf) => [o1 o2 [[[ff _] sjf] sf tf] isfo]. rewrite (ordinal_o_sr a) in pc. rewrite (ordinal_o_sr (cofinality_alt a)) in sf. have zs: sub z (substrate (ordinal_o a)) by rewrite ordinal_o_sr. move: tf; rewrite iorder_sr // => tf. set g:= Lf (Vf f) (cofinality_alt a) a. have ax: lf_axiom (Vf f) (cofinality_alt a) a. rewrite - sf;move=> t ts; apply: za; rewrite - tf; fprops. exists g;red; rewrite /g; split. by red;saw; apply: lf_function. move=> x xa; move: (pc _ xa) => [u uz xu]. rewrite -tf in uz. move: ((proj2 sjf) _ uz) => [y ysf wu]; rewrite sf in ysf. exists y=> //;rewrite LfV // - wu. move: xu => /ordo_leP [_ ua xu]. by split => //; apply: (Os_ordinal oa). move: (cofinality_pr4 oa) => [f [[[ff sf tf] cfa] [_ sif _ _]]]. set z:= Imf f. have za: sub z a by rewrite -tf; apply: Imf_Starget. have zc: cofinal (ordinal_o a) z. rewrite /cofinal (ordinal_o_sr a). split => //; move=> x xa; move: (cfa _ xa) => [y ya yp]. have wb: inc (Vf f y) a by rewrite -tf; apply: Vf_target => //;ue. exists (Vf f y). apply /(Imf_P ff); exists y => //; ue. apply /ordo_leP;split => //; by move: yp; move=> [_ _]. move: (cofinality_pr2 oa za zc). set o1:= (induced_order (ordinal_o a) z). have z1: sub z (substrate (ordinal_o a)) by rewrite ordinal_o_sr //. suff is1: (ordinal_o (cofinality a)) \Is o1. have wo1: worder (ordinal_o (cofinality a)) by fprops. have wo2: worder o1 by apply: induced_wor => //. by move: (ordinal_o_isu1 wo1 wo2 is1); rewrite ordinal_o_o // => ->. have so1: substrate o1 = z by rewrite /o1 iorder_sr //. set g:= restriction_to_image f. have sg1: source g = source f by rewrite /g /restriction_to_image /restriction2; aw. have sg: substrate (ordinal_o (cofinality a)) = source g. rewrite sg1 ordinal_o_sr //. have tg: substrate o1 = target g. by rewrite /g /restriction_to_image /restriction2 so1; aw. have bg: bijection g. apply: restriction_to_image_fb. split => //; rewrite sf;move=> x y xsf ysf => sw. have ox:=(Os_ordinal ocfa xsf). have oy:= (Os_ordinal ocfa ysf). case: (oleT_ell ox oy) => // h. by move: (sif _ _ xsf ysf h) => [_ bad]. move: (sif _ _ ysf xsf h) => [_ bad]; by case: bad. exists g; split;fprops; first by rewrite /o1; apply: (proj1 (iorder_osr _ _)). done. have ra: restriction2_axioms f (source f) (Imf f) by split => //; ue. red;rewrite sg1 => x y xsg ysg. rewrite /g /restriction_to_image restriction2_V // restriction2_V //. have wxz: inc (Vf f x) z by apply /(Imf_P ff); exists x. have wyz: inc (Vf f y) z by apply /(Imf_P ff); exists y. have wxfa: inc (Vf f x) a by apply: za. have wyfa: inc (Vf f y) a by apply: za. rewrite sf in xsg ysg. have ox:=(Os_ordinal ocfa xsg). have oy:=(Os_ordinal ocfa ysg). split. move /ordo_leP => [qa qb qc]; apply /iorder_gle0P => //; apply /ordo_leP. split => //. have h: x <=o y by []. case: (equal_or_not x y) => xy; first by rewrite xy; fprops. by move: (sif _ _ xsg ysg (conj h xy)) => [[_ _ k] _]. move /(iorder_gle0P _ wxz wyz) => h. case: (oleT_el ox oy); first by move => [_ _ h1]; apply /ordo_leP. move => h1; move: (sif _ _ ysg xsg h1) => h2. case:(oltNge h2). have [[ofy ofx _] _] := h2. by move: h; move /ordo_leP => [_ _ h3]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)