proposition: Lemma order_cp3 x y: worder x -> worder y -> ssub x y -> (segmentp y (substrate x)) -> ordinal x <o ordinal y.
proof: Proof. move => wo1 wo2 [xy xny] sp. split; [ by apply: order_cp2 | move => so ]. move: (ordinal_o_is wo2) (orderIS (ordinal_o_is wo1)); rewrite so => pa pb. move: (order_cp1 wo1 wo2 xy) => [ss xx]. move: (orderIT pa pb) => [f]; rewrite xx => isf. move: (isomorphism_to_morphism (proj1 wo2) (proj1 wo2) ss isf). set g := Lf _ _ _; move => [pc rg]. have pd: segmentp y (Imf g) by rewrite rg. move: rg; rewrite (unique_isomorphism_onto_segment wo2 pd pc) imf_ident => srr. by case: xny; rewrite xx - srr (iorder_substrate (proj1 wo2)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)