proposition: Lemma cofinality_pr5 a b: ordinalp a -> ordinalp b -> (exists2 f, cofinal_function f b a & sincr_ofn f a) -> \cf a = \cf b.
proof: Proof. move=> oa ob [f cf sif]. move: (cofinality_rw oa) => [pa pb pc]. move: (cofinality_rw ob) => [pd pe pf]. move: cf => [[ff sf tf] cf]. rewrite - sf in sif. have sif1 : forall x y, inc x a -> inc y a -> x <=o y -> Vf f x <=o Vf f y. rewrite - sf;move=> x y xa ya xy. case: (equal_or_not x y) => exy. rewrite exy; apply: oleR; apply: (Os_ordinal ob). by rewrite -tf;apply: Vf_target. by move: (sif _ _ xa ya (conj xy exy)) => [ok _]. have aux1: (cofinal_function_ex b (cofinality a)). move: pb => [g [[fg sg tg] cg]]. have cp: (f \coP g) by split => //; ue. exists (f \co g); split; first by saw; fct_tac. move => x xb. move: (cf _ xb) => [y ya xf]. move: (cg _ ya) => [z zf lzg]. have zg: inc z (source g) by ue. exists z => //; rewrite compfV //; apply: (oleT xf); apply: sif1 => //. rewrite -tg; fprops. apply: oleA; last by apply: (pf _ pa aux1). move: pe => [g [[fg sg tg] cg]]. pose h x := intersection (Zo a (fun y => Vf g x <=o Vf f y)). have hp: forall x, inc x (cofinality b) -> (inc (h x) a /\ Vf g x <=o Vf f (h x)). rewrite - sg; move => x xf; rewrite /h; set E := Zo _ _. have osE: ordinal_set E by move => t/Zo_S /(Os_ordinal oa). have vt: inc (Vf g x) b by Wtac. move: (cf _ vt) => [y y1 y2]. have ne: nonempty E by exists y; apply:Zo_i. by move/Zo_P:(ordinal_setI ne osE). have ta: lf_axiom h (cofinality b) a. by move=> t ta; move: (hp _ ta) => []. apply: (pc _ pd); exists (Lf h (cofinality b) a). split; first by red; saw; apply: lf_function. move => u ua. have wxb: inc (Vf f u) b by rewrite - tf; apply: Vf_target => //; ue. move: (cg _ wxb) => [y yb le1]; move: (hp _ yb) => [p1 p2]. exists y => //; rewrite LfV //. have le2:=oleT le1 p2. have o1:=(Os_ordinal oa ua). have o2:=(Os_ordinal oa p1). case: (oleT_el o1 o2) => // uy. rewrite sf in sif; case: (oleNgt le2 (sif _ _ p1 ua uy)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)