proposition: Lemma Exercise1_8 r r' f g: let A := Zo (substrate r) (fun z => Vf g (Vf f z) = z) in let B := Zo (substrate r') (fun z => Vf f (Vf g z) = z) in increasing_fun f r r' -> increasing_fun g r' r -> (induced_order r A) \Is (induced_order r' B).
proof: Proof. move=> A B [o1 o2 [ff sf tf] incf][_ _ [fg sg tg] incg]. have p1: (forall x, inc x A -> inc (Vf f x) B). by move=> x /Zo_P [xsr r1]; apply: Zo_i; [Wtac | rewrite r1]. have p2: (forall x, inc x B -> inc (Vf g x) A). by move=> x /Zo_P [xsr r1]; apply: Zo_i ; [Wtac | rewrite r1]. have Ha: source (restriction2 f A B) = A by rewrite / restriction2; aw. have Hb: target (restriction2 f A B) = B by rewrite / restriction2; aw. have asf: sub A (source f) by rewrite sf; apply: Zo_S. set (h:=restriction2 f A B). have ra: (restriction2_axioms f A B). split => //. rewrite /B -tf; apply: Zo_S. by move => t /(Vf_image_P ff asf) [s sa ->]; apply: p1. have fh: function h by apply: (proj31 (restriction2_prop ra)). have ih: (injection h). split=> //; rewrite Ha; move => x y xA yA /=. rewrite /h restriction2_V // restriction2_V // => eq. move: xA yA => / Zo_hi <- /Zo_hi <-; ue. have sh: (surjection h). split => //; rewrite Ha Hb; move=> y yB. move: (p2 _ yB) => wA. ex_tac; move: yB => /Zo_P [ysr ww]; rewrite /h restriction2_V //. have As: (sub A (substrate r)) by apply: Zo_S. have Bs: (sub B (substrate r')) by apply: Zo_S. have Ash: A = source h by rewrite /h; aw. have Bsh: B = target h by rewrite /h; aw. move: (iorder_osr o1 As) => [pa pb]. move: (iorder_osr o2 Bs) => [pc pd]. exists h; split => //; first by rewrite pb pd; split. red;rewrite -Ash; move=> x y xA yA. rewrite /h restriction2_V // restriction2_V //; aw; try apply: p1 => //. split. move =>aux; apply /iorder_gle0P; try apply: p1 => //. apply: (incf _ _ (iorder_gle1 aux)). move =>aux; apply /iorder_gle0P => //. move: (incg _ _ (iorder_gle1 aux)). by move: xA yA => /Zo_hi -> /Zo_hi ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)