proposition: Lemma isomorphism_to_morphism f r r' x (F := (Lf (Vf f) (substrate r) (substrate r'))): order r -> order r' -> sub x (substrate r') -> order_isomorphism f r (induced_order r' x) -> (order_morphism F r r' /\ Imf F = x).
proof: Proof. move=> oa ob sxa [ou ov' [bf sz tz] siz]. rewrite iorder_sr // in tz. have fh: function f by fct_tac. have ta1: lf_axiom (Vf f) (substrate r) (substrate r'). move=> t tu; apply: sxa; Wtac. have fF: function F by apply: lf_function. have rg: Imf F = x. rewrite - tz; set_extens t. move/(Imf_P fF); rewrite /F; aw; move => [a asf ->]; rewrite LfV//; Wtac. move/(proj2 (proj2 bf)) => [u us ->]. by rewrite sz in us;apply/(Imf_P fF); rewrite /F; aw; ex_tac; rewrite LfV. split =>//; split => //; first by rewrite /F;split;aw. rewrite /F;hnf; aw;move => x1 x2 x1s x2s; rewrite !LfV//. rewrite - sz in x1s x2s; apply: (iff_trans (siz _ _ x1s x2s)). split; first by move/iorder_gle1. move => hh; apply/iorder_gle0P => //; rewrite - tz; Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)