proposition: Lemma opowa_invariant r1 r2 r3 r4: worder r1 -> worder r2 -> worder r3 -> worder r4 -> r1 \Is r2 -> r3 \Is r4 -> (olexp r1 r3) \Is (olexp r2 r4).
proof: Proof. move: r1 r2 r3 r4. pose H13 r1 r3 := worder r1 /\ worder r3. pose C3 r1 r3 := triple (substrate r3) (substrate r1). pose s13 r1 r3 := substrate (olexp r1 r3). have s1p: forall r1 r3 x, H13 r1 r3 -> inc x (s13 r1 r3) -> let C := C3 r1 r3 x in [/\ function C, source C = (substrate r3), target C = substrate r1 & graph C = x]. move=> r1 r3 x [wor1 wor3]. rewrite /s13 (proj2 (olexp_osr wor1 wor3)) => /Zo_P; move=> [pa _]. rewrite /C3; aw;split => //; move /(gfunctions_P2): pa => [p1 p2 p3]. apply: function_pr => //. have cpp: forall r1 r2 r3 r4 f g1, H13 r1 r3 -> order_isomorphism f r1 r2 -> order_isomorphism g1 r4 r3 -> forall x, inc x (s13 r1 r3) -> let C := C3 r1 r3 x in [/\ f \coP C, function (f \co C), ((f \co C) \coP g1), function ((f \co C) \co g1) & source ((f \co C) \co g1) = (substrate r4) /\ target ((f \co C) \co g1) = (substrate r2)]. move => r1 r2 r3 r4 f g h13 isf isg x xsr C; aw. move: isf => [o1 o2 [bf sf tf] orf]. move: isg => [o3 o4 [bg sg tg] org]. move; move: (s1p _ _ _ h13 xsr) => [fc sc tc gc]. have p1: f \coP C by split => //;[ fct_tac| ue]. have p2: function (f \co C) by fct_tac. have p3: ((f \co C) \coP g) by split => //; aw;try fct_tac; rewrite/C /C3; aw. split => //;fct_tac. pose h3 r1 r3 f g x := graph (f \co (C3 r1 r3 x) \co g). have ax3: forall r1 r2 r3 r4 f g x, H13 r1 r3 -> H13 r2 r4 -> order_isomorphism f r1 r2 -> order_isomorphism g r4 r3 -> inc x (s13 r1 r3) -> inc (h3 r1 r3 f g x) (s13 r2 r4). move => r1 r2 r3 r4 f g x h13 [wo2 wo4] isf isg. move: (h13) => [wo1 wo3]. move: (isf) => [o1 o2 [bf sf tf] orf]. move: (isg) => [o3 o4 [bg sg tg] org]. move=> xs; move: (s1p _ _ _ h13 xs) ; set C := C3 r1 r3 x. move => [fc sc tc gc]. have sctg: (source C = target g) by rewrite /C /C3; aw. have o12g: sub (olexp_I r1 r3 x) (target g). by move=> t; rewrite tg; apply: Zo_S. move: (cpp _ _ _ _ _ _ h13 isf isg _ xs) => [p1 p2 p3 p4 [p5 p6]]. rewrite /s13 (proj2 (olexp_osr wo2 wo4)); apply: Zo_i. by rewrite -p5 -p6; apply: gfunctions_i. set s:= olexp_I _ _ _. have qz: forall t, inc t (substrate r4) -> inc (Vf g t) (source C). move => t ts4. have s3: inc t (source g) by aw;ue. rewrite sctg; aw; apply Vf_target =>//; fct_tac. set l2 := olexp_lE r2; set l1 := olexp_lE r1. have fg: function g by fct_tac. have qa: s = Zo (substrate r4) (fun i => Vf f (Vf C (Vf g i)) <> l2). set_extens t => /Zo_P [q1 q2]; apply /Zo_P;split => //; move: q2; rewrite /h3 -/(Vf (f \co C \co g) t) => //; rewrite - sg in q1; rewrite ! compfV //; Wtac. have qb: s = Zo (substrate r4) (fun i => (Vf C (Vf g i)) <> l1). rewrite qa; set_extens t => /Zo_P [q1 q2]; apply/Zo_P;split => //;move: q2. set u := Vf C (Vf g t). case: (equal_or_not u l1) => // h1; case. have ur1: inc u (substrate r1). by rewrite -tc; apply: Vf_target => //; apply: qz. have ne1: nonempty (substrate r1) by ex_tac. rewrite /l2/olexp_lE; move:(image_of_inf wo1 wo2 isf ne1) => [qc <-]; ue. set u := Vf C (Vf g t) => h; dneg h1. have ur1: inc u (substrate r1). by rewrite - tc; apply: Vf_target => //; apply: qz. have ne1: nonempty (substrate r1) by ex_tac. rewrite /l2/olexp_lE; move: (image_of_inf wo1 wo2 isf ne1) => [qc]. have <-: l2 = the_least r2 by done. rewrite -h1 => sv. move: bf => [[ff fi] _]; apply: fi => //; ue. set g1:= inverse_fun g. have ss1: sub (olexp_I r1 r3 x) (source g1) by rewrite /g1; aw. have p0: bijection g1 by apply: inverse_bij_fb. have fg1: function g1 by fct_tac. have -> : s = Vfs g1 (olexp_I r1 r3 x). rewrite qb; set_extens t. move => /Zo_P; rewrite {1} /Vf corresp_g ;move=> [ts4 tv]. apply /(Vf_image_P fg1 ss1); exists (Vf g t) => //. apply /Zo_P;split => //; Wtac. by rewrite inverse_V2 //; ue. move => /(Vf_image_P fg1 ss1) [u /Zo_P]. have ->: substrate r4 = target g1 by rewrite /g1; aw. move => [pa pb] ->; apply /Zo_P; split. Wtac;rewrite /g1; aw; ue. by rewrite - tg in pa; rewrite (inverse_V bg); rewrite /C /C3 /Vf; aw. apply: finite_image_by => //. by move: xs; rewrite /s13 (proj2 (olexp_osr wo1 wo3)) // => /Zo_P [_]. move=> r1 r2 r3 r4 wo1 wo2 wo3 wo4 [f isf] [g isg]. move: (inverse_order_is isg) => isg1. move: (inverse_order_is isf) => isf1. have h13a: H13 r1 r3 by split. have h24a: H13 r2 r4 by split. set g1 := inverse_fun g; set f1 := inverse_fun f. pose h := h3 r1 r3 f g1. pose hi := h3 r2 r4 f1 g. set srs := substrate (olexp r1 r3); set srt:= substrate (olexp r2 r4). have ax: forall x, inc x srs -> inc (h x) srt. move => x srx. by move: (ax3 r1 r2 r3 r4 f g1 x h13a h24a isf isg1 srx). have ax': forall x, inc x srt -> inc (hi x) srs. move => x srx. by move: (ax3 r2 r1 r4 r3 f1 g x h24a h13a isf1 isg srx). move: (isf) => [o1 o2 [bf sf tf] orf]. move: (isg) => [o3 o4 [bg sg tg] org]. have sg1: source g1 = substrate r4 by rewrite /g1 ; aw. have tg1: target g1 = substrate r3 by rewrite /g1 ; aw. have sf1: source f1 = substrate r2 by rewrite /f1 ; aw. have tf1: target f1 = substrate r1 by rewrite /f1 ; aw. have p0: bijection g1 by apply: inverse_bij_fb. have hin: forall x y, inc x srs -> inc y srs -> h x = h y -> x = y. rewrite /h;move=> x y xs ys sh. move: (cpp _ _ _ _ _ _ h13a isf isg1 _ xs) => [p1 p2 p3 p4 [p5 p6]]. move: (cpp _ _ _ _ _ _ h13a isf isg1 _ ys) => [q1 q2 q3 q4 [q5 q6]]. have pa: ((f \co C3 r1 r3 x) \co g1) = ((f \co C3 r1 r3 y) \co g1). by apply: function_exten1 => //; rewrite p6 q6 //. move: (fct_co_simpl_right p3 q3 p0 pa) => pb. move: (fct_co_simpl_left p1 q1 bf pb); rewrite /C3 => pc. by move: (f_equal graph pc); aw. have hs: forall y, inc y srt -> exists2 x, inc x srs & y = h x. move=> y ysr. move: (ax' _ ysr) => aux. move: (s1p r2 r4 y h24a ysr); set z:= C3 r2 r4 y; move => [s1 s2 s3 s4]. move: (s1p r1 r3 _ h13a aux);set w:= C3 _ _ _; move=> [s1' s2' s3' s4']. exists (hi y) => //; rewrite /h /h3; rewrite -/w. rewrite - s4; apply f_equal. move: (cpp _ _ _ _ _ _ h13a isf isg1 _ aux). rewrite -/w -/g1; move => [p1 p2 p3 p4 [p5 p6]]. move: (cpp _ _ _ _ _ _ h24a isf1 isg _ ysr). rewrite -/f1 -/z; move => [q1 q2 q3 q4 [q5 q6]]. have: w = f1 \co z \co g. rewrite /w /hi /h3 -/z. move: q4 => [q4 _ _]; rewrite - {2} (corresp_recov1 q4) /C3. by rewrite -q5 - q6; aw. move => ->. set a := (f1 \co z). have c1: f \coP a. rewrite /a /f1;red; aw; split => //; fct_tac. rewrite (compfA c1 q3). have c2: f \coP f1 by apply: composable_f_inv. have c3: g \coP g1 by apply: composable_f_inv. have c4: z \coP g by split => // ; [fct_tac | rewrite s2; ue]. have ->: f \co a = z. rewrite /a compfA // bij_right_inverse //. have ->: target f = target z by rewrite s3; ue. rewrite compf_id_l //. rewrite - compfA // bij_right_inverse //. have ->: target g = source z by rewrite s2; ue. rewrite compf_id_r //. move: (olexp_osr wo1 wo3) => [oa os13]. move: (olexp_osr wo2 wo4) => [ob os24]. exists (Lf h srs srt); saw; rewrite ? os13 ? os24. saw; apply: lf_bijective => //. have hp: forall z i, inc z srs -> inc i (substrate r4) -> Vg (h z) i = Vf f (Vg z (Vf g1 i)). move => z i zrs isr. move: (cpp _ _ _ _ _ _ h13a isf isg1 _ zrs) => [q1 q2 q3 q4 [q5 q6]]. rewrite - sg1 in isr. have w1: inc (Vf g1 i) (source (C3 r1 r3 z)). rewrite /C3; aw; rewrite - tg1; Wtac; fct_tac. by rewrite /h /h3 -/(Vf _ i) ! compfV//; rewrite {2} /Vf /C3; aw. have p1: olexp_G r1 r3 = srs by ue. have p2: olexp_G r2 r4 = srt by ue. red; aw. move => x y xsr ysr; rewrite !LfV//;split. move => /(olexp_gleP wo1 wo3); rewrite p1; move => [xi yi cxy]. apply /(olexp_gleP wo2 wo4); rewrite p2;split => //; try (apply: ax => //). case: cxy => cxy; first (by rewrite cxy; left); right. move: cxy => [j [js3 ltj eqj]]. have wj4: inc (Vf g j) (substrate r4) by rewrite - tg; Wtac; fct_tac. have jv: Vf g1 (Vf g j) = j by rewrite inverse_V2 //; ue. exists (Vf g j); split => //. by rewrite hp // hp // jv; apply :(order_isomorphism_sincr isf). move => i ip. have i4:inc i (substrate r4) by order_tac. rewrite hp // hp //; congr (Vf f _); apply: eqj. by rewrite - jv; apply : (order_isomorphism_sincr isg1). move => /(olexp_gleP wo2 wo4); rewrite p2; move => [xi yi cxy]. apply /(olexp_gleP wo1 wo3); rewrite p1;split => //. case: cxy => cxy; first (by left; apply hin); right. move: cxy => [j [js4 ltj eqj]]. have wj4: inc (Vf g1 j) (substrate r3) by rewrite - tg1;Wtac;fct_tac. have jv: Vf g (Vf g1 j) = j by rewrite inverse_V //; ue. have xyi: forall i, inc i (substrate r3) -> (inc (Vg x i) (substrate r1) /\ inc (Vg y i) (substrate r1)). move=> i isr; split. move: xsr; rewrite -p1 => /Zo_P [] /gfunctions_P2 [q1 q2 q3] _. apply: q3; apply /(range_gP q1); rewrite q2; ex_tac. move: ysr; rewrite -p1 => /Zo_P [] /gfunctions_P2 [q1 q2 q3] _. apply: q3; apply /(range_gP q1); rewrite q2; ex_tac. exists (Vf g1 j); split => //. move: (ltj); move: (xyi _ wj4); rewrite - sf; move => [s1 s2]. by rewrite hp // hp //; move /(order_isomorphism_siso isf s1 s2). move => i ip. have i4:inc i (substrate r3) by order_tac. have wi: inc (Vf g i) (substrate r4) by rewrite - tg; Wtac; fct_tac. have i5: glt r4 j (Vf g i) by rewrite -jv; apply (order_isomorphism_sincr isg). move: (eqj _ i5). move: (xyi _ i4); rewrite - sf; move => [s1 s2]. move: bf => [[_ isf2] _]. have iv: Vf g1 (Vf g i) = i by rewrite inverse_V2 //; ue. by rewrite hp // hp // iv; apply: isf2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)