proposition: Lemma Exercise1_11f r r': order r -> order r' -> nonempty (substrate r) -> complete_lattice (increasing_mappings_order r r') -> complete_lattice r'.
proof: Proof. move => or or' nes clf; apply: Exercise1_11b =>//. set (E:= substrate r); set (E':=substrate r'). move: (imo_osr r or') => [oim sr1]. move=> X XE'. set (Y:= Zo (substrate (increasing_mappings_order r r')) (fun f => exists2 y, inc y X & f = constant_function E E' y)). have Ys: (sub Y (substrate (increasing_mappings_order r r'))) by apply: Zo_S. move: clf => [_ clf']; move: (clf' _ Ys)=> [[f fs] _]. move:fs => /(lubP oim Ys). rewrite {1} /upper_bound sr1. move => [] [] /soimP [[ff sf tf] incf] fg fge. move: (nes) => [x xE]. set (u:= Vf f x). have uE' : (inc u E') by rewrite /E' /u; Wtac. exists u; apply /(lubP or' XE'); split. split => // y yE; move:(XE' _ yE) => yE'. set (g:= constant_function E E' y). have gy: (inc g Y). apply: Zo_i; [by rewrite sr1; apply: constant_increasing | ex_tac]. move: (fg _ gy) => /(imo_gleP _ or') [_ _]. by move=> [[p1 p2 p3] [p4 p5 p6] p7]; move: (p7 _ xE);rewrite /g constant_V. move=> z [zs zu]. set (g:= (constant_function E E' z)). have gs: inc g (increasing_mappings r r') by apply: constant_increasing. have aux: (upper_bound (increasing_mappings_order r r') Y g). split; first by rewrite sr1. move=> y /Zo_P [ys [v vX ->]]. by rewrite -/g - constant_increasing1//; [ apply: zu | apply:XE']. move: (fge _ aux) => /(imo_gleP _ or') [_ _] [[p1 p2 p3] [p4 p5 p6] p7]. move: (p7 _ xE);rewrite /g constant_V //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)