proposition: Lemma distributive_lattice_prop2: [/\ (distributive_lattice3 r -> distributive_lattice4 r), (distributive_lattice3 r -> distributive_lattice1 r) & (distributive_lattice3 r -> distributive_lattice2 r)].
proof: Proof. move:(lattice_props lr). set (E:= substrate r). move: (lr) => [or _]. move => [sE [iE [sixy [isxy [sxyz [ixyz [sxx [ixx [sxyx ixyx]]]]]]]]]. have p1: (distributive_lattice3 r -> distributive_lattice4 r). move => h x y z xE yE zE zx. move: (h _ _ _ xE yE zE). rewrite (inf_comparable1 or zx)(sup_comparable1 or zx). rewrite (sixy _ _ yE zE) (inf_C r (sup r y z) x). rewrite (ixyz _ _ _ (sE _ _ xE yE) xE (sE _ _ yE zE)). rewrite (sup_C r x y) (isxy _ _ yE xE) sup_C//. split; first by exact. move=> d3 x y z xE yE zE. move: (d3 _ _ _ xE yE zE) => ab;move: (f_equal (sup r x) ab). set (t := sup r x (inf r (sup r x y) (inf r (sup r y z) (sup r z x)))). move: (iE _ _ xE yE) (iE _ _ yE zE) (iE _ _ zE xE) => ixyE iyzE izxE. rewrite (sxyz _ _ _ xE ixyE (sE _ _ iyzE izxE)). rewrite (sup_C r x _) (inf_C r x y) (sixy _ _ yE xE). rewrite (sup_C r (inf r y z) (inf r z x)). rewrite (sxyz _ _ _ xE izxE iyzE) (sup_C r x (inf r z x)) (sixy _ _ zE xE). move=> ->. rewrite /t. rewrite (sup_C r x z); set sxy:= sup r x y; set szx:= sup r z x. have xsxy:gle r x sxy by move: (lattice_sup_pr lr xE yE)=> [q1 q2 q3]. have sxyE: inc sxy (substrate r) by order_tac. rewrite ((p1 d3) _ _ _ sxyE (iE _ _ (sE _ _ yE zE) (sE _ _ zE xE)) xE xsxy). apply: f_equal. rewrite sup_C inf_C -/szx. have xsrx:gle r x szx by move: (lattice_sup_pr lr zE xE)=> [q1 q2 q3]. have szxE: inc szx (substrate r) by order_tac. rewrite ((p1 d3) _ _ _ szxE (sE _ _ yE zE) xE xsrx). rewrite -(sxyz _ _ _ yE zE xE) -/szx inf_C; apply: isxy => //. move=> d3 x y z xE yE zE. move: (d3 _ _ _ xE yE zE) => ab;move: (f_equal (inf r x) ab). set (t := inf r x (sup r (inf r x y) (sup r (inf r y z) (inf r z x)))). move: (sE _ _ xE yE) (sE _ _ yE zE) (sE _ _ zE xE) => sxyE syzE szxE. rewrite (ixyz _ _ _ xE sxyE (iE _ _ syzE szxE)). rewrite (inf_C r x _) (sup_C r x y) (isxy _ _ yE xE). rewrite (inf_C r (sup r y z) (sup r z x)). rewrite (ixyz _ _ _ xE szxE syzE) (inf_C r x (sup r z x)) (isxy _ _ zE xE). move=> <-; rewrite /t. rewrite (inf_C r x z); set ixy:= inf r x y; set izx:= inf r z x. have xsxy:gle r ixy x by move: (lattice_inf_pr lr xE yE)=> [q1 q2 q3]. have ixyE: inc ixy (substrate r) by order_tac. rewrite sup_C. rewrite -((p1 d3) _ _ _ xE (sE _ _ (iE _ _ yE zE) (iE _ _ zE xE)) ixyE xsxy). apply: f_equal. have xsrx:gle r izx x by move: (lattice_inf_pr lr zE xE)=> [q1 q2 q3]. have izxE: inc izx (substrate r) by order_tac. rewrite -((p1 d3) _ _ _ xE (iE _ _ yE zE) izxE xsrx). rewrite inf_C -(ixyz _ _ _ yE zE xE) . rewrite -/izx sup_C sixy //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)