proposition: Lemma distributive_lattice_prop4: (distributive_lattice3 r <-> distributive_lattice6 r).
proof: Proof. move: (lr) => [or _]. move:(lattice_props lr) =>/=. set (E:= substrate r). move => [sE [iE [sixy [isxy [sxyz [ixyz [sxx [ixx [sxyx ixyx]]]]]]]]]. split => aux. move=> x y z xE yE zE. move: (sE _ _ xE yE)(iE _ _ xE yE) => sxyE ixyE. move: (distributive_lattice_prop2) => [_ _ il2]. rewrite ((il2 aux) _ _ _ sxyE zE ixyE). rewrite (inf_C r (sup r x y) z) ((il2 aux) _ _ _ zE xE yE)(inf_C r y z). have ->: (inf r (sup r x y) (inf r x y) = inf r x y). rewrite inf_C; apply: inf_comparable1 => //. move: (lattice_sup_pr lr xE yE) (lattice_inf_pr lr xE yE). move=> [p1 _ _] [p2 _ _]; order_tac. rewrite sup_C; apply: f_equal; rewrite sup_C //. apply /distributive_lattice_prop3; move=> x y z xE yE zE. rewrite (inf_C r z (sup r x y)). move: (aux _ _ _ xE yE zE). move: (sE _ _ xE yE)(iE _ _ xE yE); set (b:= sup r x y); set (xy:= inf r x y). move=> bE xyE. move: (lattice_inf_pr lr bE zE)=> [z1 z2 z3]. move: (lattice_sup_pr lr zE xyE)=> [w1 w2 w3]. set A:= inf r _ _; set B := sup r _ _. have l1: gle r (inf r (sup r x y) z) A. rewrite /A;move: (lattice_inf_pr lr bE (sE _ _ zE xyE)). move=> [q1 q2 q3]; apply: q3 => //; order_tac. move: (iE _ _ yE zE)(iE _ _ zE xE); set (yz:= inf r y z); set (zx:= inf r z x). move=> yzE zxE. have l2: gle r B (sup r x yz). rewrite /B. move: (lattice_sup_pr lr xE yzE) => [q1 q2 q3]. move: (lattice_sup_pr lr xyE (sE _ _ yzE zxE))=> [_ _]; apply. move: (lattice_inf_pr lr xE yE) => [h _ _]; order_tac. move: (lattice_sup_pr lr yzE zxE) => [_ _ ]; apply;first by exact. move: (lattice_inf_pr lr zE xE) => [_ h _]; order_tac. move=> AB; rewrite AB in l1; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)