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