proposition: Lemma ordinal_le_P x x': ordinal_leD1 x x' <-> [/\ ordinalp x, ordinalp x' & exists f S, segmentp (ordinal_o x') S /\ order_isomorphism f (ordinal_o x) (induced_order (ordinal_o x') S)].
proof: Proof. split. move=> [or or' [otr otr' [f [t [sx iso]]]]];split => //. move: (isomorphism_worder_sub (ordinal_o_wor or') sx) =>[]. set g := iso_seg_fun _ _ => sw isg; exists (g \co f), (target g); split => //. exact: (compose_order_is iso isg). move=> [or or' [f [t [[sx sxp] oi]]]]; split => //; split; fprops. by exists f, t. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)