proposition: Lemma setX_lattice_sup g (r := order_product g) x y (z := sup r x y) (t := inf r x y): order_fam g -> (allf g lattice) -> inc x (substrate r) -> inc y (substrate r) -> [/\ inc z (substrate r), inc t (substrate r), (forall i, inc i (domain g) -> Vg z i = sup (Vg g i)(Vg x i) (Vg y i)) & (forall i, inc i (domain g) -> Vg t i = inf (Vg g i)(Vg x i) (Vg y i))].
proof: Proof. move => ofg alg xsr ysr. move: (setX_lattice ofg alg) => []; rewrite -/r => or hr. move: (hr _ _ xsr ysr); set xy:= doubleton x y; move => [hs hi]. have zsr: inc z (substrate r). by move: (sup_pr or xsr ysr hs) => [pa _ _]; rewrite /z; order_tac. have tsr: inc t (substrate r). by move: (inf_pr or xsr ysr hi) => [pa _ _]; rewrite /t; order_tac. move: (xsr) (ysr); rewrite {1 2} (proj2(order_product_osr ofg)) => xsr1 ysr1. have sd: sub xy (prod_of_substrates g) by move=> u; case /set2_P => ->. move: (sup_in_product ofg sd) => [pa pb]. move: hs;rewrite -pa; move => hs; move: (pb hs) => hz. move: (inf_in_product ofg sd) => [pc pd]. move: hi;rewrite -pc; move => hi; move: (pd hi) => ht. clear pa pb pc pd hs hi. have fgf: fgraph (fam_of_substrates g) by rewrite /fam_of_substrates; fprops. have aidf: forall i, inc i (domain g) -> [/\ inc i (domain (fam_of_substrates g)), function (pr_i (fam_of_substrates g) i), sub xy (source (pr_i (fam_of_substrates g) i)) & Vfs (pr_i(fam_of_substrates g) i) xy = doubleton (Vg x i) (Vg y i)]. move => i idg. have id: inc i (domain (fam_of_substrates g)). by rewrite /fam_of_substrates; aw. have fp: function (pr_i (fam_of_substrates g) i) by fprops. have sxy: sub xy (source (pr_i (fam_of_substrates g) i)). by rewrite /pr_i; aw. split => //; set_extens u. move => /(Vf_image_P fp sxy) [w wxy ->]. move: (sxy _ wxy); rewrite {1} /pr_i lf_source => ws. rewrite pri_V //; move: wxy;case /set2_P => ->; fprops. have ixxy: inc x xy by rewrite /xy; fprops. have iyxyy: inc y xy by rewrite /xy; fprops. by case /set2_P=> ->; apply /(Vf_image_P fp sxy); [exists x | exists y] => //;rewrite pri_V. split => //. move => i idg; move: (f_equal (Vg^~ i) hz); rewrite !LgV//; move => ->. by move: (aidf _ idg) => [qa qb qc ->]. move => i idg; move: (f_equal (Vg^~i) ht); rewrite !LgV//; move => ->. by move: (aidf _ idg) => [qa qb qc ->]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)