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