proposition: Lemma bij_pair_isomorphism_onto_segment r r' f f': worder r -> worder r' -> segmentp r' (Imf f) -> order_morphism f r r' -> segmentp r (Imf f') -> order_morphism f' r' r -> (order_isomorphism f r r' /\ order_isomorphism f' r' r /\ f = inverse_fun f').
proof: Proof. move=> wor wor' sr1 om sr2 om'. move: (om)(om')=>[or or' [ff sf tf] fp] [_ _ [ff' sf' tf'] fp']. have gf: sgraph (graph f) by fprops. have gf': sgraph (graph f') by fprops. have cff': (f \coP f') by split => //; ue. have cf'f: (f' \coP f) by split => //; ue. have mor1 := (compose_order_morphism om' om). have mor2 := (compose_order_morphism om om'). have fc: function (f' \co f) by fct_tac. have srg: segmentp r (Imf (f'\co f)). split. have <-: target (f' \co f) = substrate r by aw. by apply: Imf_Starget. move=> x y. rewrite (ImfE fc) /compose; aw; rewrite (compg_range _ gf). move/dirim_P=> [u urg p2] yx. have xrg: (inc x (Imf f')) by rewrite (ImfE ff');ex_tac. have usr: inc u (source f') by Wtac. move: ((proj2 sr2) _ _ xrg yx) => /(Imf_P ff') [v vsf' vp]. move: yx; rewrite (Vf_pr ff' p2) vp -fp'// => yr. rewrite -(ImfE ff) in urg *. move: ((proj2 sr1) _ _ urg yr) => va; apply /dirim_P; ex_tac; Wtac. have srg': segmentp r' (Imf (f \co f')). have fc': function (f \co f') by fct_tac. split. have <-: target (f \co f') = substrate r' by aw. by apply: Imf_Starget. move => x y. rewrite (ImfE fc') /compose; aw; rewrite (compg_range _ gf'). move/dirim_P=> [u urg p2] yx. have xrg: (inc x (Imf f)) by rewrite (ImfE ff); ex_tac. have usr: inc u (source f) by Wtac. move: ((proj2 sr1) _ _ xrg yx) => /(Imf_P ff) [v vsf' vp]. move: yx; rewrite (Vf_pr ff p2) vp -fp// => yr. rewrite -(ImfE ff') in urg *. move: ((proj2 sr2) _ _ urg yr) => va; apply /dirim_P; ex_tac; Wtac. have p1 := (unique_isomorphism_onto_segment wor srg mor2). have p2 := (unique_isomorphism_onto_segment wor' srg' mor1). rewrite - sf in p1; rewrite - sf' in p2. have [p3 p4 p5] := (bijective_from_compose cff' cf'f p2 p1). by split. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)