proposition: Lemma Exercise1_11c g: order_fam g -> (allf g complete_lattice) -> complete_lattice (order_product g).
proof: Proof. move=> alo ala. move: (order_product_osr alo) => [og Ha]. apply: Exercise1_11b => // X Xsr. set f := Lg (domain g) (fun i => substrate (Vg g i)). have fgf: fgraph f by rewrite /f; fprops. have fpri: forall i, inc i (domain g) -> function (pr_i f i). move=> i idg;apply: pri_f; rewrite /f; aww. have pf: productb f = substrate (order_product g) by rewrite Ha. pose Xi i := (Vfs (pr_i f i) X). have p1: forall i, inc i (domain g) -> sub (Xi i) (substrate (Vg g i)). move => i idg; rewrite /Xi. have <-: (target (pr_i f i) = substrate (Vg g i)). by rewrite /pr_i/f; aw; rewrite LgV//. apply: fun_image_Starget1; apply: (fpri _ idg). set v:= Lg (domain g) (fun i => supremum (Vg g i) (Xi i)). have v1: forall i, inc i (domain g) -> least_upper_bound (Vg g i)(Xi i)(Vg v i). move=> i idg; rewrite /v LgV//; move: (ala _ idg) => [_ ila]. by move: (ila _ (p1 _ idg)) => [hs _]; apply: supremum_pr1=> //; apply: alo. have vs: (inc v (substrate (order_product g))). rewrite Ha; apply /prod_of_substratesP;rewrite /v; split;aww. move=> i idg; rewrite LgV//. move: (v1 _ idg) => /(lubP (alo _ idg)(p1 _ idg)). rewrite /v LgV//; move => [[ok _] _] //. exists v; apply /(lubP og Xsr); split. split => // y yX; apply /order_product_gleP; rewrite -Ha;split => //. by apply: Xsr. move=> i idg; move: (v1 _ idg) => /(lubP (alo _ idg)(p1 _ idg)). move=> [[p3 p2] _]; apply: p2. have yp: inc y (productb f) by rewrite pf; apply: Xsr. have idf: inc i (domain f) by rewrite /f; aw. apply /(Vf_image_P) => //; first by apply: pri_f. by rewrite /pr_i; rewrite lf_source pf. rewrite - (pri_V idf yp); ex_tac; apply: W_pr3. move => z [zs zu]; apply /order_product_gleP => //; rewrite -Ha;split => //. move=> i idg; move: (v1 _ idg). move/ (lubP (alo _ idg)(p1 _ idg));move=> [p2]; apply. split. move: zs; rewrite -pf => /prod_of_substratesP [q1 q2 q3]. by move: (q3 _ idg);aw. have sX: sub X (source (pr_i f i)) by rewrite /pr_i; aw;ue. move: (fpri _ idg) => fi. move=> y /(Vf_image_P fi sX) [u uX ->]. have up: inc u (productb f) by rewrite pf; apply: Xsr. have idf: inc i (domain f) by rewrite /f; aw. rewrite (pri_V idf up). by move: (zu _ uX) => /order_product_gleP [_ _]; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)