proposition: Lemma Exercise1_14 A B R (rho := fun X => Zo B (fun y => forall x,inc x X -> inc (J x y) R)) (sigma := fun Y => Zo A (fun x => forall y, inc y Y -> inc (J x y) R)) (fr:=Lf rho (\Po A) (\Po B)) (fs:= Lf sigma (\Po B) (\Po A)) (iA := subp_order A) (iB := subp_order B): sub R (A \times B) -> [/\ decreasing_fun fr iA iB, decreasing_fun fs iB iA, closure (compose fs fr) iA & closure (compose fr fs) iB].
proof: Proof. move=> sR. have ta: (lf_axiom rho (\Po A) (\Po B)). move=> t ts; apply /setP_P; apply: Zo_S. have tb: (lf_axiom sigma (\Po B) (\Po A)). move=> t ts; apply /setP_P; apply: Zo_S. have tc: forall t, sub t A -> sub (rho t) B. by move=> t /setP_P ta1; apply /setP_P; apply: ta. have td: forall t, sub t B -> sub (sigma t) A. by move=> t /setP_P ta1; apply /setP_P; apply: tb. have ffr: (function fr) by apply: lf_function. have ffs: (function fs) by apply: lf_function. have c1: (fs \coP fr) by split => //; rewrite /fs/fr; aw. have c2: (fr \coP fs) by split => //; rewrite /fs/fr; aw. have fc1: (function (fs \co fr)) by fct_tac. have fc2: (function (fr \co fs)) by fct_tac. have i1: (forall u v, sub u v -> sub (rho v) (rho u)). move=> u v uv t => /Zo_P [pa pb]; apply: Zo_i => //; fprops. have i2: (forall u v, sub u v -> sub (sigma v) (sigma u)). move=> u v uv t => /Zo_P [pa pb]; apply: Zo_i => //; fprops. have i3: (forall u v, sub u v -> sub (sigma (rho u)) (sigma (rho v))). by move=> u v uv; apply: i2; apply: i1. have i4: (forall u v, sub u v -> sub (rho (sigma u)) (rho (sigma v))). by move=> u v uv; apply: i1; apply: i2. move: (subp_osr A) (subp_osr B)=> [oA sA] [oB sB]. have pa:decreasing_fun fr iA iB. split => //; rewrite /fr; aw; first by saw. move=> x y /subp_gleP [xA yA xy]; rewrite !LfV//; try apply /setP_P => //. apply /subp_gleP;split;fprops. have pb:decreasing_fun fs iB iA. split => //; rewrite /fs;aw ; first by saw. move=> x y /subp_gleP [xA yA xy]; rewrite ! LfV//; try apply /setP_P => //. apply /subp_gleP;split;fprops. have Ha: forall x, sub x A -> sub x (sigma (rho x)). move=> x xA t tx; apply: Zo_i; first by apply: xA. by move=> y /Zo_P [yB h]; apply: h. have Hb: forall x, sub x B -> sub x (rho (sigma x)). move=> x xA t tx; apply:Zo_i; first by apply: xA. by move=> y /Zo_P [yB h]; apply: h. have ic1: (increasing_fun (fs \co fr) iA iA). split => //; rewrite /fr/fs; first by saw. move=> x y /subp_gleP [xA yA xy]. have sa: inc x (\Po A) by apply /setP_P. have sb: inc y (\Po A) by apply /setP_P. rewrite !compfV//; aw; trivial;rewrite (LfV ( c := x)) // (LfV ( c := y)) //. rewrite ! LfV//; try apply: ta => //. apply /subp_gleP;split;fprops. have ic2: (increasing_fun (fr \co fs) iB iB). split => //; rewrite /fr/fs; aw; first by saw. move=> x y /subp_gleP [xA yA xy]. have sa: inc x (\Po B) by apply /setP_P. have sb: inc y (\Po B) by apply /setP_P. rewrite !compfV//; aw; trivial; rewrite (LfV ( c := x)) // (LfV ( c := y)) //. rewrite ! LfV//; try apply: tb => //. apply /subp_gleP;split;fprops. split => //; split => //. + move=> x; rewrite sA => xA; move: (xA); move /setP_P => xA'. rewrite /fr compfV//;aw; trivial; rewrite LfV// /fs LfV//; last by apply: ta. apply /subp_gleP;split => //;[ by apply: td; apply: tc | by apply: Ha]. + rewrite sA;move=> x xA; set y := Vf (fs \co fr) x. move: (xA) => /setP_P xA'. have xs: inc x (source fr) by rewrite /fr; aw. have yv: (y = sigma (rho x)). by rewrite /y compfV // /fr LfV// /fs LfV//; apply: ta. have yA: sub y A by rewrite yv;apply: td; apply: tc. move : (yA) => /setP_P => yA'. have ys: inc y (source fr) by rewrite /fr; aw. rewrite compfV// /fr LfV// /fs LfV//; last by apply: ta. suff ->: (rho y = rho x) by symmetry. by rewrite yv;apply: extensionality; [apply: i1; apply: Ha | apply: Hb; apply: tc]. + move=> x; rewrite sB => xB; move: (xB); move /setP_P => xB'. have xx: inc x (source fs) by rewrite /fs; aw. rewrite compfV// /fs LfV// /fr LfV//; last by apply: tb. apply /subp_gleP;split => //;[ by apply: tc; apply: td | by apply: Hb]. + rewrite sB;move=> x xB; set y := Vf (fr \co fs)x. move: (xB) => /setP_P xB'. have xs: inc x (source fs) by rewrite /fs; aw. have yv: (y = rho (sigma x)). by rewrite /y compfV// /fs LfV// /fr LfV//; apply: tb. have yB: sub y B by rewrite yv;apply: tc; apply: td. move : (yB) => /setP_P => yB'. have ys: inc y (source fs) by rewrite /fs; aw. rewrite compfV // /fs LfV// /fr LfV//; last by apply: tb. suff ->: (sigma y = sigma x) by symmetry. by rewrite yv;apply: extensionality; [apply: i2; apply: Hb | apply: Ha; apply: td]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)