proposition: Lemma Exercise1_6n: nonempty E -> (lattice r' <-> lattice (increasing_mappings_order r r')).
proof: Proof. move=> ne1; split. move:(imo_osr r or') => [pa pb]. move=> sl; split => //; rewrite pb. move=> x y xs ys. move: (xs)(ys) => /soimP [[fx sx tx] ix] /soimP [[fy sy ty] iy]. have Ha: forall c, inc c E -> (inc (Vf x c) F) /\ (inc (Vf y c) F). move => c cE; rewrite /F -{1} tx - ty;split; apply: Vf_target =>//; ue. have ta1: (lf_axiom (fun i=> sup r' (Vf x i) (Vf y i)) E F). move => c cE; move: (Ha _ cE) => [w1 w2]. move: (lattice_sup_pr sl w1 w2)=> [aux _ _]; rewrite /F; order_tac. have ta2: (lf_axiom (fun i=> inf r' (Vf x i) (Vf y i)) E F). move => c cE; move: (Ha _ cE) => [w1 w2]. move: (lattice_inf_pr sl w1 w2)=> [aux _ _]; rewrite /F; order_tac. set (f1:= Lf (fun i=> sup r' (Vf x i) (Vf y i)) E F). set (f2:= Lf (fun i=> inf r' (Vf x i) (Vf y i)) E F). have ff1: (function f1) by rewrite /f1; apply: lf_function. have ff2: (function f2) by rewrite /f1; apply: lf_function. have fp1: function_prop f1 E F by rewrite/f1; saw. have fp2: function_prop f2 E F by rewrite/f2; saw. have if1:increasing_fun f1 r r'. split => //; rewrite /f1; aw => u v uv. have uE: (inc u E) by rewrite /E;order_tac. have vE: (inc v E) by rewrite /E;order_tac. move:(Ha _ uE)(Ha _ vE) => [uxE uyE] [vxE vyE]. rewrite !LfV//. move: (lattice_sup_pr sl uxE uyE) (lattice_sup_pr sl vxE vyE). move=> [p1 p2 p3] [p4 p5 p6]. have le1:(gle r' (Vf x u) (Vf x v)) by apply: (proj44 ix). have le2:(gle r' (Vf y u) (Vf y v)) by apply: (proj44 iy). apply: p3; order_tac. have if2:increasing_fun f2 r r'. split => //; rewrite /f2. move=> u v uv. have uE: (inc u E) by rewrite /E;order_tac. have vE: (inc v E) by rewrite /E;order_tac. move:(Ha _ uE)(Ha _ vE) => [uxE uyE] [vxE vyE]. rewrite !LfV//;move:(lattice_inf_pr sl uxE uyE) (lattice_inf_pr sl vxE vyE). move=> [p1 p2 p3] [p4 p5 p6]. have le1:(gle r' (Vf x u) (Vf x v)) by apply: (proj44 ix). have le2:(gle r' (Vf y u) (Vf y v)) by apply: (proj44 iy). apply: p6; order_tac. have sif1: inc f1 (increasing_mappings r r'). rewrite /f1;apply /soimP=> //;saw; saw. have sif2: inc f2 (increasing_mappings r r'). rewrite /f2;apply /soimP=> //;saw; saw. move: (imo_osr r or') => [o2 s2]. have sd:sub (doubleton x y) (substrate (increasing_mappings_order r r')). by move=> t; case /set2_P => -> //; rewrite s2. split. exists f1; apply /lubP =>//;split. split; first by rewrite s2. move=> u; case /set2_P => ->; apply /imo_gleP => //;split => //. split => //; rewrite /f1; move => i isr; rewrite LfV //. by move: (Ha _ isr) => [wxe wye];case: (lattice_sup_pr sl wxe wye). split => //;rewrite /f1; move => i isr; rewrite LfV //. by move: (Ha _ isr) => [wxe wye];case: (lattice_sup_pr sl wxe wye). move=> z [z1 z2]. move: (imo_incr or' (z2 _ (set2_1 x y))) => inx. move: (z2 _ (set2_2 x y)) => /(imo_gleP _ or') [_ p1 [xx fz hh]]. rewrite /f1; apply /(imo_gleP _ or');split => //;split => //; aw. move=> i isr; rewrite LfV //. move: (inx _ isr) (hh _ isr) => r1 r2; move:(Ha _ isr) => [xwe ywe]. by move: (lattice_sup_pr sl xwe ywe)=> [r3 r4]; apply. exists f2; apply /glbP=> //;split. split; first by rewrite s2 //. move=> u; case /set2_P => ->; apply /(imo_gleP _ or');split => //. rewrite /f2; saw;try saw. move => i isr; rewrite LfV //; move:(Ha _ isr) => [xwe ywe]. by case: (lattice_inf_pr sl xwe ywe). rewrite /f2;saw; try saw; move => i isr; rewrite LfV //. by move:(Ha _ isr) => [xwe ywe];case: (lattice_inf_pr sl xwe ywe). move=> z [z1 z2]. move: (imo_incr or' (z2 _ (set2_1 x y))) => inx. move: (z2 _ (set2_2 x y)) => /(imo_gleP _ or') [p1 p2 [p3 p4 p5]]. rewrite /f2; apply /(imo_gleP _ or');split => //; saw. move=> i isr; rewrite LfV => //; move:(Ha _ isr) => [xwe ywe]. move: (inx _ isr) (p5 _ isr) => r1 r2. by move: (lattice_inf_pr sl xwe ywe)=> [r3 r4]; apply. move=> sl; split; first by exact. move=> x y xsr ysr. set (f1:= constant_function E F x). set (f2:= constant_function E F y). have f1s: (inc f1 (increasing_mappings r r')) by apply: constant_increasing. have f2s: (inc f2 (increasing_mappings r r')) by apply: constant_increasing. move:(proj2 (imo_osr r or')) => sr2. move: (f1s)(f2s); rewrite - sr2 => f1si f2si. set (r''':= increasing_mappings_order r r') in *. have sd:sub (doubleton x y) (substrate r') by move=> t; case /set2_P=> ->. move: (ne1) => [t te]. split. move: (lattice_sup_pr sl f1si f2si) => [l1 l2 l3]. have: (inc (sup r''' f1 f2) (substrate r''')) by order_tac. rewrite {2} /r''' sr2 => /soimP [[fs ss ts] ifs]. set z := Vf (sup r''' f1 f2) t. have wt: (inc z F) by rewrite /z/F -ts; Wtac; ue. have xz: gle r' x z. move: (imo_incr or' l1 te); rewrite {1} /f1 constant_V //. have yz: gle r' y z. move: (imo_incr or' l2 te); rewrite {1} /f1 constant_V //. exists z; apply /lubP => //; split. split; [ exact | by move=> u; case /set2_P => ->]. move=> u [usr um]. set (f4:= constant_function E F u). have f4s:(inc f4 (increasing_mappings r r')) by apply: constant_increasing. have f14: (gle (increasing_mappings_order r r') f1 f4). rewrite /f1/f4 /E/F - constant_increasing1 //; apply: um; fprops. have f24: (gle (increasing_mappings_order r r') f2 f4). rewrite /f1/f4 /E/F - constant_increasing1 //; apply: um; fprops. by move: (imo_incr or' (l3 _ f14 f24) te);rewrite -/r'' -/z /f4 constant_V. move: (lattice_inf_pr sl f1si f2si) => [l1 l2 l3]. have: (inc (inf r''' f1 f2) (substrate r''')) by order_tac. rewrite {2} /r''' sr2;move /soimP => [[fs ss ts] ifs]. set z := Vf (inf r''' f1 f2) t. have wt: (inc z F) by rewrite /z/F -ts; Wtac; ue. have yz: gle r' z y by move: (imo_incr or' l2 te); rewrite {1} /f1 constant_V. have xz: gle r' z x by move: (imo_incr or' l1 te); rewrite {1} /f1 constant_V. exists z; apply /glbP => //; split. split; [ exact | by move=> u; case /set2_P => ->]. move=> u [usr um]. set (f4:= constant_function E F u). have f4s:(inc f4 (increasing_mappings r r')) by apply: constant_increasing. have f14: (gle (increasing_mappings_order r r') f4 f1). rewrite /f1/f4 /E/F - constant_increasing1 //; apply: um; fprops. have f24: (gle (increasing_mappings_order r r') f4 f2). rewrite /f1/f4 /E/F - constant_increasing1 //; apply: um; fprops. by move: (imo_incr or' (l3 _ f14 f24) te); rewrite -/r'' -/z /f4 constant_V. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)