proposition: Lemma ordinal_lt_P x x': ordinal_ltD1 x x' <-> [/\ ordinalp x, ordinalp x' & exists f y', inc y' x' /\ order_isomorphism f (ordinal_o x) (induced_order (ordinal_o x') (segment (ordinal_o x') y') )].
proof: Proof. split; last first. move => [or or' [f [y [sx isof]]]]; apply /ordinal_lt_P1; split => //. move:(proj1 (ordinal_o_wor or)) (proj1 (ordinal_o_wor or')) => o1 o2. set t := segment (ordinal_o x') y. have sxs: sub t (substrate (ordinal_o x')) by apply: sub_segment. case: (isomorphism_to_morphism o1 o2 sxs isof). by set g := Lf _ _ _; exists g, y. move /ordinal_lt_P1. set r := (ordinal_o x); set r':= (ordinal_o x'). move=> [or or' [f [y [pa pb pc]]]]; split => //. move: pc (order_morphism_fi pc) => [oa oc [ff sf tf] isof] injf. move: (restriction_to_imageE ff) => eq. set g := restriction_to_image f. have tg : target g = segment r' y. rewrite /g eq /restriction1; aw; trivial;rewrite - pb - ImfE //. have Xs: sub (target g) (substrate r') by rewrite tg; apply: sub_segment. have [or1 sr1 ] := (iorder_osr oc Xs). move: (restriction_to_image_fb injf) => bg; move: (proj1(proj1 bg)) => fg. have ss: source f = source g by rewrite /g eq /restriction1; aw. have aux: forall x, inc x (source g) -> Vf g x = Vf f x. move => t xsf; rewrite /g eq restriction1_V //; ue. exists g, y; rewrite - tg;split => //; split => //;first by split => //; ue. move => u v usg vsg; move: (usg)(vsg); rewrite - ss => usf vsf. apply:(iff_trans (isof _ _ usf vsf)); rewrite - (aux _ usg) - (aux _ vsg). split => pd; [by apply/iorder_gle0P => //; Wtac | exact: (iorder_gle1 pd) ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)