proposition: Lemma scompl_unique r x y: boolean_lattice r -> inc x (substrate r) -> complement_pr r x (the_greatest r) y -> y = standard_completion r x.
proof: Proof. move=> blr xsr h1. move: (scompl_pr blr xsr) => h2. move: blr => [bl1 bl2 bl3]. move: (bl1) => [[or _] _ _]. move: (proj2 (the_greatest_pr or bl2) _ xsr) => xg. by move: (Exercise1_17a bl1 bl3 xg) => /unique_existence [_]; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)