proposition: Lemma regular_cofinal_si_unique z: uniqueness (fun x => regular_ordinal x /\ (exists2 f, cofinal_function f z x & sincr_ofn f x)).
proof: Proof. set H := fun x => _. suff: forall x y, H x -> H y -> x <=o y. by move=> ht x y hx hy; apply: oleA;apply: ht. move=> x y [rx [f fx sif]] [ry [g gy sig]] {H}. move: fx gy => [[ff sf tf] fp] [[fg sg tg] gp]. pose h t := choose (fun z => inc z x /\ Vf g t <=o (Vf f z)). have htp: forall t, inc t y -> (inc (h t) x /\ Vf g t <=o (Vf f (h t))). move=> t ty; apply choose_pr. have wz: inc (Vf g t) z by rewrite - tg; apply: Vf_target => //; ue. by move: (fp _ wz) => [u u1 u2]; exists u. have ta: lf_axiom h y x by move=> t ty; move: (htp _ ty) => []. move: rx ry => [ox rx] [oy _]. move: (cofinality_rw ox) => [_ _ aux]; rewrite -rx; apply: (aux _ oy). exists (Lf h y x). split; first by split => //;aw; trivial;apply: lf_function. move=> t tx. have wz: inc (Vf f t) z by rewrite - tf; apply: Vf_target => //; ue. move: (gp _ wz) => [u zu le1]. move: (htp _ zu) => [wy le2]. have le3:= oleT le1 le2. ex_tac; rewrite LfV//. case: (oleT_el (Os_ordinal ox tx) (Os_ordinal ox wy)) => //. move => le4; case: (oleNgt le3 (sif _ _ wy tx le4)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)