proposition: Lemma least_greatest_pr1 r a: boolean_lattice r -> inc a (substrate r) -> [/\ sup r (the_least r) a = a, inf r a (the_greatest r) = a, inf r (the_least r) a = (the_least r) & sup r a (the_greatest r) = (the_greatest r)].
proof: Proof. move=> [[[or _] el _] eg _] asr. move: (least_greatest_pr or) => [h1 h2 h3 h4];split; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)