proposition: Lemma ordinal_lt_pr2 a b: worder b -> ordinal_ltD1 a (ordinal b) -> exists f x, [/\ inc x (substrate b), Imf f = segment b x & order_morphism f (ordinal_o a) b].
proof: Proof. move=> ob /ordinal_lt_P1 [oa op [f [x [xsp rgx om]]]]. have [g oig]: order_isomorphic (ordinal_o (ordinal b)) b. by apply: orderIS; apply: (ordinal_o_is ob). move: om (oig) => [o1 o2 [ff sf tf] pf][_ o4 [[gi gs] sg tg] pg]. have cfg: g \coP f by split => //; try fct_tac; ue. rewrite ! ordinal_o_sr in sf tf sg. have p0: function (g \co f) by fct_tac. have p3: order_morphism (g \co f) (ordinal_o a) b. split=> //; first by saw; rewrite ordinal_o_sr. hnf; aw; move=> u v asf bsf; rewrite ! compfV //. apply: (iff_trans (pf _ _ asf bsf)); apply/ pg; rewrite sg - tf; Wtac. set y:= (Vf g x). have p1: inc y (substrate b) by rewrite /y;Wtac; fct_tac. exists (g \co f), y; split => //. set_extens u. move /(Imf_P p0)=> [v vsf ->]. rewrite compf_s in vsf. have /segmentP xx : inc (Vf f v) (segment (ordinal_o (ordinal b)) x). by rewrite -rgx; Wtac. by rewrite compfV //;apply /segmentP; apply (order_isomorphism_sincr oig). move/segmentP=> buy. have utg: inc u (target g) by rewrite tg; order_tac. move: ((proj2 gs) _ utg) buy => [v vsg ->]. rewrite - sg in xsp. move/(order_isomorphism_siso oig vsg xsp) => /segmentP. rewrite -rgx; move/(Imf_P ff) => [w pa pb]. apply/(Imf_P p0); aw; ex_tac; rewrite pb; rewrite compfV //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)