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