proposition: Lemma scompl_pr r x: boolean_lattice r -> inc x (substrate r) -> complement_pr r x (the_greatest r) (standard_completion r x).
proof: Proof. move=> [rr eg dl3] xsr; move: (rr) => [[or _] _ _]. apply:the_complement_pr => //. exact: (proj2(the_greatest_pr or eg) _ xsr). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)