proposition: Lemma scomplI r x: boolean_lattice r -> inc x (substrate r) -> standard_completion r (standard_completion r x) = x.
proof: Proof. move=> blr xsr; move: (scompl_pr blr xsr). rewrite /complement_pr sup_C inf_C ;move => [ysr ym yq]. symmetry; apply: scompl_unique => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)