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