proposition: Lemma inclusion_morphism_a a b (f:= Lf id a b) : a <=o b -> ( segmentp (ordinal_o b) (Imf f) /\ order_morphism f (ordinal_o a) (ordinal_o b)).
proof: Proof. move => [oa ob ab]. have s1: segmentp (ordinal_o b) a. rewrite /segmentp (ordinal_o_sr b). split; [exact | move => s t; aw ]. move /(oltP oa) => su /ordo_leP [tv sv ts]. have ot:= (Os_ordinal ob tv). have os:= (Os_ordinal ob sv). apply /(oltP oa); apply: ole_ltT su; split => //. split; first by rewrite (ci_range ab). rewrite /f; split; fprops. rewrite !ordinal_o_sr;hnf;aw; split => //; fprops. red; aw;move => x y xa ya; rewrite ! LfV//; split. move => /ordo_leP [tv sv ts]; apply /ordo_leP;split;fprops. move => /ordo_leP [tv sv ts]; apply /ordo_leP;split;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)