fact: Definition distributive_lattice4 r := forall x y z, inc x (substrate r) ->inc y (substrate r) -> inc z (substrate r) -> gle r z x -> sup r z (inf r x y) = inf r x (sup r y z).
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)