proposition: Lemma distributive_lattice_prop3: (distributive_lattice3 r <-> distributive_lattice5 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: (distributive_lattice_prop2) => [p1 p2 p3]. move=> x y z xE yE zE. rewrite (p3 aux) // (inf_C r z y). move: (iE _ _ yE zE) (iE _ _ zE xE); set b:= inf r y z. move=> bE izxE. move: (lattice_sup_pr lr xE bE) => [q1 q2 q3]. move: (lattice_sup_pr lr izxE bE)=> [_ _]; apply => //. apply: order_transitivity q1 => //. by move: (lattice_inf_pr lr zE xE) => [r1 r2 r3]. move: (distributive_lattice_prop1) => [h _]; apply: h. move => x y z xE yE zE. move: (iE _ _ yE zE) (sE _ _ xE zE) (sE _ _ xE yE) => iyzE sxzE sxyE. apply: (order_antisymmetry or). move: (lattice_sup_pr lr xE (iE _ _ yE zE)) => [q1 q2 q3]. move: (lattice_inf_pr lr yE zE) => [r1 r2 _]. move: (lattice_inf_pr lr sxyE sxzE) => [_ _]; apply. move: (lattice_sup_pr lr xE yE) => [p1 p2 p3]. apply: q3 => //; apply: order_transitivity p2 => //. move: (lattice_sup_pr lr xE zE) => [p1 p2 p3]. apply: q3 => //; apply: order_transitivity p2 => //. move: (aux _ _ _ xE yE zE). move: (aux _ _ _ xE zE (sE _ _ xE yE)). set (a:= inf r (sup r x y) (sup r x z)). set (b:= sup r x (inf r y z)). set (c:= inf r z (sup r x y)). move=> le1 le2. move: (lattice_sup_pr lr xE iyzE); rewrite -/b; move=> [le3 _ _]. move: (lattice_sup_pr lr xE (iE _ _ zE sxyE) ); rewrite -/c; move=> [_ _ hc]. apply: (order_transitivity or le1 (hc _ le3 le2)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)