proposition: Lemma Exercise2_7g u v: inc u (closures) -> inc v (closures) -> Jf (u \co v) -> has_supremum (closure_ordering) (doubleton u v).
proof: Proof. move=> uc vc Jcuv. have Ht:sub (doubleton u v) (closures). by move=> t /set2_P;case => ->. move: (uc) (vc); move => /Zo_P [p1 p2] /Zo_P [p3 p4]. move: p2 p4=> [q1 q2 q3] [q4 q5 q6]. have Ha: forall x, inc x E -> inc (Vf u x) E. move=> x xE; move: (q2 _ xE) => aux; rewrite /E; order_tac. have Hb: forall x, inc x E -> inc (Vf v x) E. move=> x xE; move: (q5 _ xE) => aux; rewrite /E; order_tac. move: p1 p3 =>/functionsP [fu su tu] /functionsP [fv sv tv]. have cp: u \coP v by split => //;ue. set f := u \co v. have ff: (function f) by rewrite /f; fct_tac. set (gg := fun x => the_least (induced_order r (Ixf x f))). have sI: (forall x, inc x E -> sub (Ixf x f) (substrate r)). move=> x xE; apply: Zo_S. have sI1: forall x, inc x E -> substrate(induced_order r (Ixf x f)) = (Ixf x f). move=> x xE; move: (sI _ xE) => aux; rewrite iorder_sr //. have lg: forall x, inc x E -> least (induced_order r (Ixf x f)) (gg x). move=> x xE; move: (Jcuv _ xE) => ey. apply: the_least_pr => //; apply: (proj1 (iorder_osr or (sI _ xE))). have gp: forall x, inc x E -> [/\ inc (gg x) (substrate r), gle r x (gg x), Vf f (gg x) = gg x & (forall y, inc y (Ixf x f) -> gle r (gg x) y)]. move=> x xE; move: (lg _ xE);rewrite /least; rewrite (sI1 _ xE). move => [] /Zo_P [pa [pb pc]] p2; split => //. move=> y yI; move: (p2 _ yI) => h;apply: (iorder_gle1 h). have ta:(lf_axiom gg E E). by move=> t tE; move: (gp _ tE) => [ok _]. have p0P: forall x, inc x E -> ((gg x = x) <-> (Vf f x = x)). move=> x xE; move: (gp _ xE) => [p1 p2 p3 p4]. split => h; first by rewrite -h. have xI: inc x (Ixf x f) by apply: Zo_i => //; split => //; order_tac. move: (p4 _ xI) => p5; order_tac. have p1: (forall x, inc x E -> gle r x (gg x)). by move=> x xE; move: (gp _ xE) => [_ ]. have p2: (forall x, inc x E -> gg (gg x) = gg x). by move=> x xE; apply /(p0P _ (ta _ xE)); move: (gp _ xE) => [_ _]. have p3: forall x y, gle r x y -> gle r (gg x) (gg y). move=> x y xy. have xE:(inc x E) by rewrite /E;order_tac. have yE:(inc y E) by rewrite /E;order_tac. move: (gp _ yE) => [s1 s2 s3 s4]. have gyI: (inc (gg y) (Ixf x f)) by apply: Zo_i => //; split => //; order_tac. by move: (gp _ xE) => [_ _ _]; apply. set (g:= Lf gg E E). have fg: (function g) by apply: lf_function. have cg: (closure g r). split => //; rewrite /g. split => //; first by saw. move=> x y xy. have xx: gle r (gg x) (gg y) by apply:p3. rewrite !LfV///E; order_tac. by move=> x xE;rewrite LfV//; apply: p1. by move=> x xE; rewrite (LfV ta xE) (LfV ta (ta _ xE)); apply: p2. move: (Exercise2_7b) => [oco sco]. have hco: inc g closures by apply: Zo_i => //; apply /functionsP; split => //; rewrite /g;aw. have hsco: inc g (substrate (closure_ordering)) by rewrite sco. have sd: sub (doubleton u v) (substrate closure_ordering) by ue. have sg: source g = E by rewrite /g;aw. have sf: source f = E by rewrite /f; aw. have ig: fixpoints g = fixpoints f. set_extens t => /Zo_P []; rewrite ?sf ? sg => [r1 r2]; apply /Zo_P;split => //; try ue; move : r2; rewrite /g LfV//; move /(p0P _ r1) => //. have sif: fixpoints f = (fixpoints u) \cap (fixpoints v). rewrite /fixpoints su sv sf; set_extens t. move /Zo_P => [tE wf]. have tsv: inc t (source v) by ue. have Wtsv: inc (Vf v t) (substrate r) by rewrite -/E -tv; fprops. move: wf; rewrite /f compfV// => wf. move: (f_equal (fun z=> Vf u z) wf); rewrite q3 // wf => f1. move: (q2 _ Wtsv) (q5 _ tE); rewrite wf => le1 le2. apply /setI2_P; split => //; apply /Zo_P;split => //;order_tac. move /setI2_P => [] /Zo_P [tE Wu] /Zo_P [_ Wv]; apply /Zo_P;split => //. by rewrite /f compfV// ?sv // Wv Wu. exists g. apply /(lubP oco sd); split. split => //; move=> y ys. have aux: inc y closures by rewrite - sco; apply: sd. by apply /(Exercise2_7dP aux hco); case /set2_P: ys => ->; rewrite ig sif => t /setI2_P []. move=> z [ze zh]. have zc: inc z closures by ue. move: (zh _ (set2_1 u v)) (zh _ (set2_2 u v)). move /(Exercise2_7dP uc zc) => h1 /(Exercise2_7dP vc zc) => h2. apply (Exercise2_7dP hco zc);rewrite ig sif. move => t ts; apply: setI2_i;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)