proposition: Lemma ordinal_le_P1 x x': ordinal_leD1 x x' <-> [/\ ordinalp x, ordinalp x' & exists2 f, segmentp (ordinal_o x') (Imf f) & order_morphism f (ordinal_o x)(ordinal_o x')].
proof: Proof. split; last first. move=> [or or' [f _ mf]]; split => //. move:(proj1 (ordinal_o_wor or)) (proj1 (ordinal_o_wor or')) => o1 o2. by apply /(order_le_alt o1 o2); exists f. move /ordinal_le_P => [or or' [f [t [sx isof]]]]; split => //. move:(proj1 (ordinal_o_wor or)) (proj1 (ordinal_o_wor or')) => o1 o2. have sxs: sub t (substrate (ordinal_o x')) by apply: sub_segment1. move: sx;case: (isomorphism_to_morphism o1 o2 sxs isof) => h <-. by set g := Lf _ _ _; exists g. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)