proposition: Lemma distributive_lattice_prop1: ( (distributive_lattice1 r -> distributive_lattice3 r) /\ (distributive_lattice2 r -> distributive_lattice3 r)).
proof: Proof. move:(lattice_props lr). set (E:= substrate r). move => [sE [iE [sixy [isxy [sxyz [ixyz [sxx [ixx [sxyx ixyx]]]]]]]]]. split. move=> d1 x y z xE yE zE. move: (iE _ _ yE zE) (sE _ _ xE yE) => iyzE sxyE. rewrite (d1 _ _ _ iyzE zE xE) (sup_C r (inf r y z) x). rewrite (d1 _ _ _ xE yE zE) (sup_C r x z) (sixy _ _ yE zE). set (sxy :=sup r x y); set (syz:=sup r y z); set (szx:= sup r z x). have ->:(inf r z (inf r sxy szx) = inf r z sxy). rewrite (inf_C r sxy szx) (ixyz _ _ _ zE (sE _ _ zE xE) sxyE). rewrite (inf_C r z (sup r z x)) (sup_C r z x) (isxy _ _ xE zE) //. rewrite (d1 _ _ _ (iE _ _ xE yE) zE sxyE) (sup_C r _ z). rewrite (d1 _ _ _ zE xE yE) (sup_C r z y) (sup_C r (inf r x y) _). rewrite (d1 _ _ _ sxyE xE yE). rewrite (sxyx _ _ xE yE) {2} (sup_C r x y) (sxyx _ _ yE xE). rewrite (sup_C r y x) (ixx _ sxyE) inf_C (inf_C r syz szx) //. move=> d1 x y z xE yE zE. move: (sE _ _ yE zE) (iE _ _ xE yE) => syzE ixyE. rewrite (d1 _ _ _ syzE zE xE) (inf_C r (sup r y z) x). rewrite (d1 _ _ _ xE yE zE) (inf_C r x z) (isxy _ _ yE zE). set (ixy := inf r x y); set (iyz:= inf r y z); set (izx:= inf r z x). have ->:(sup r z (sup r ixy izx) = sup r z ixy). rewrite (sup_C r ixy izx) (sxyz _ _ _ zE (iE _ _ zE xE) ixyE). rewrite (sup_C r z (inf r z x)) (inf_C r z x) (sixy _ _ xE zE) //. rewrite (d1 _ _ _ (sE _ _ xE yE) zE ixyE) (inf_C r _ z). rewrite (d1 _ _ _ zE xE yE) (inf_C r z y) (inf_C r (sup r x y) _). rewrite (d1 _ _ _ ixyE xE yE). rewrite (ixyx _ _ xE yE) {2} (inf_C r x y) (ixyx _ _ yE xE). rewrite (inf_C r y x) (sxx _ ixyE) sup_C (sup_C r iyz izx) //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)