proposition: Lemma order_le_compatible r r' r1 r1': r \Is r1 -> r' \Is r1' -> (r <=O r' <-> r1 <=O r1').
proof: Proof. move: r r' r1 r1'. suff: forall r1 r2 r3 r4, r1 \Is r3 -> r2 \Is r4 -> r1 <=O r2 -> r3 <=O r4. by move=> aux r1 r2 r3 r4 p1 p2; split;apply: aux=>//; apply: orderIS. move => r1 r2 r3 r4 /orderIS [f [o3 _ [[injf srf] sf tf] oif]]. move=> [g [_ o4 [[ig srg] sg tg] oig]]. move=> [o1 o2 [h [X [sX [_ _ [[ih srh] sh th] oih]]]]]. split => //. set Y:= Vfs g X. have sY: sub Y (substrate r4) by rewrite -tg; apply:fun_image_Starget1; fct_tac. move: (proj1 srf) (proj1 srg) (proj1 srh) => ff fg fh. have sX': sub X (source g) by ue. have Yp1: forall x, inc x X -> inc (Vf g x) Y. move=> x xX; apply /(Vf_image_P fg sX'); ex_tac. have Yp2: forall y, inc y Y -> exists2 x, inc x X & y = Vf g x. by move=> y; move/(Vf_image_P fg sX'). move: th; rewrite iorder_sr // => th. pose k x := Vf g (Vf h (Vf f x)). have ta1: forall x, inc x (substrate r3) -> inc (k x) Y. rewrite - sf => t ts; apply: Yp1;Wtac; rewrite sh -tf; Wtac. exists (Lf k (substrate r3) Y), Y; split => //. have aux: bijection (Lf k (substrate r3) Y). apply: lf_bijective => //. rewrite - sf => u v us vs eq. move: (Vf_target ff us) (Vf_target ff vs); rewrite tf - sh => Wt1 Wt2. move: (Vf_target fh Wt1)(Vf_target fh Wt2); rewrite th; aw => Wt3 Wt4. move: (proj2 ig);rewrite sg => bi. move: (bi _ _ (sX _ Wt3) (sX _ Wt4) eq) => eq1. move: ((proj2 ih) _ _ Wt1 Wt2 eq1) => eq2. by apply: (proj2 injf). move=> t tY; move: (Yp2 _ tY) => [x xX ->]. rewrite - th in xX; move: ((proj2 srh) _ xX)=> [v vsf ->]. rewrite sh - tf in vsf; move: ((proj2 srf) _ vsf)=> [w wsc ->]. rewrite - sf; ex_tac. move: (iorder_osr o4 sY) => [or4 sr4]. split; [exact | exact| by rewrite sr4 /bijection_prop; aw | ]. hnf; aw; move=> u v us vs; rewrite !LfV //. rewrite - sf in us vs; apply: (iff_trans (oif _ _ us vs)). move: (Vf_target ff us) (Vf_target ff vs); rewrite tf - sh => Wt1 Wt2. move: (Vf_target fh Wt1)(Vf_target fh Wt2); rewrite th => Vt1 Vt2. move: (sX' _ Vt1) (sX' _ Vt2) => U1 U2; move: (Yp1 _ Vt1)(Yp1 _ Vt2) => X1 X2. apply: (iff_trans (oih _ _ Wt1 Wt2)). apply: (iff_trans(iorder_gle0P r2 Vt1 Vt2)). apply: (iff_trans (oig _ _ U1 U2)); symmetry; exact: iorder_gle0P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)