proposition: Lemma order_transportation f r (r':= Vfs (f \ftimes f) r) : bijection f -> order_on r (source f) -> order_isomorphism f r r'.
proof: Proof. move=> [[ff injf] [_ sjf]] [or sr]. have gr: sgraph r by fprops. have ffp: function_prop f (substrate r) (target f) by rewrite sr. move:(ext_to_prod_fun_bis ffp ffp) => [fe se te]. have aux: sub r (source (ext_to_prod f f)). by rewrite se; apply:sub_graph_coarse_substrate. set (E:= source f). have zr': (forall z,inc z r' <-> (exists x y, [/\ inc x E, inc y E, inc (J x y) r & z = J (Vf f x) (Vf f y)])). move => z; rewrite /r'; split. move /(Vf_image_P fe aux) => [x xr]. move:(pr1_sr xr)(pr2_sr xr); rewrite sr => pxs pys. have Jg := (gr _ xr). rewrite -Jg (ext_to_prod_V ff ff pxs pys) => ->. by exists (P x), (Q x); rewrite Jg. move=> [x [y [xE yE Jr zJ]]]; apply /(Vf_image_P fe aux); ex_tac. move:(arg1_sr Jr)(arg2_sr Jr); rewrite sr => xs ys. by rewrite (ext_to_prod_V ff ff xs ys). have gr': sgraph r' by move=> z /zr'; move=> [x [y [_ _ _ ->]]]; fprops. have sr': substrate r' = target f. set_extens t. + case /(substrate_P gr') => [] [y] /zr'[u [v [uE vE Jr zJ]]]. by rewrite (pr1_def zJ); fprops. by rewrite (pr2_def zJ); fprops. + move/sjf => [x xsf Wt]. apply: (@arg1_sr _ t t); apply/ zr'; exists x; exists x. rewrite Wt; split=> //; order_tac; ue. suff or': order r'. hnf;split => // x y xsr ysr; split. by move =>h;apply /zr'; exists x, y. move/zr' => [x' [y' [xE' yE' pr sj]]]. move: (pr12_def sj) => [w1 w2]. by rewrite (injf _ _ xsr xE' w1)(injf _ _ ysr yE' w2). split; first exact. - move => y;rewrite sr' => yr; apply/zr'. move: (sjf _ yr) => [x xsf Wt]. exists x, x; rewrite Wt; split => //; order_tac; ue. - move=>x y z /zr' [a [b [aE bE J1r Jab]]] /zr' [c [d [cE dE J2r Jcd]]]. apply/zr'; exists a, d. have bc: (b = c). by apply: injf =>//;rewrite - (pr2_def Jab) - (pr1_def Jcd). rewrite bc in J1r. by rewrite - (pr1_def Jab)- (pr2_def Jcd); split => //; order_tac. - move=> x y /zr' [a [b [aE bE J1r Jab]]] /zr' [c [d [cE dE J2r Jcd]]]. move:(pr12_def Jab) (pr12_def Jcd)=> [xva yvb][yvc xvd]. have Wbc: Vf f b = Vf f c by rewrite - yvb. have Wad: Vf f a = Vf f d by rewrite - xva. move:(injf _ _ bE cE Wbc) (injf _ _ aE dE Wad) => eq1 eq2. rewrite xva yvc. have -> // : c = d by rewrite eq1 eq2 in J1r; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)