proposition: Lemma the_complement_pr r x y: relatively_complemented r -> distributive_lattice3 r -> gle r x y -> complement_pr r x y (the_complement r x y).
proof: Proof. move => pa pb pc. move: (Exercise1_17a pa pb pc) => /unique_existence [[z zv] pe]. have pf: exists2 x0, inc x0 (substrate r) & complement_pr r x y x0. by exists z => //; case: zv. have pg: singl_val2 (inc^~ (substrate r)) (complement_pr r x y). by move => a b qa qb qc qd; apply: pe. exact: (proj1(select_pr pf pg)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)