proposition: Lemma ordinal_lt_P1 x x': ordinal_ltD1 x x' <-> [/\ ordinalp x, ordinalp x' & exists f y, [/\ inc y x', Imf f = segment (ordinal_o x') y & order_morphism f (ordinal_o x) (ordinal_o x')]].
proof: Proof. split. move => [] /ordinal_le_P1 [or or' [f srf om]] nrr'. case: (well_ordered_segment (ordinal_o_wor or') srf). move => rgf;case: nrr'; apply: ordinal_o_isu => //. have injf:= (order_morphism_fi om). have [o1 o2 [ff sf tf] mf] := om. exists f; split => //; split => //. split => //;apply: surjective_pr1; [fct_tac |rewrite tf rgf //]. move=> [t xsr rgf]. split => //; exists f, t; split => //. by rewrite - (ordinal_o_sr x'). move=> [or or' [f [t [xsr rgf om]]]]. have wodr := (ordinal_o_wor or'). have odr := proj1 wodr. have p1: segmentp (ordinal_o x') (Imf f). by rewrite rgf;apply: segment_segment =>//; rewrite ordinal_o_sr //. split; first by apply /ordinal_le_P1 => //; split => //;exists f. move=> rr'; rewrite rr' in om. move: (unique_isomorphism_onto_segment wodr p1 om); rewrite ordinal_o_sr => idf. by case:(@not_in_segment (ordinal_o x') t); rewrite - rgf idf imf_ident. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)