fact: Definition lattice r := order r /\ forall x y, inc x (substrate r) -> inc y (substrate r) -> (has_supremum r (doubleton x y) /\ has_infimum r (doubleton x y)).
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)