proposition: Lemma Exercise1_17a r x y: relatively_complemented r -> distributive_lattice3 r -> gle r x y -> exists! x', complement_pr r x y x'.
proof: Proof. move => [lr el ec] dl3 xy; move: (lr) => [or _]. apply /unique_existence; split. by move:(ec _ _ xy) => [z za];exists z. move=> u v [us su iu][vs sv iv]. move:(lattice_props lr). set (E:= substrate r). move => [sE [iE [sixy [isxy [sxyz [ixyz [sxx [ixx [sxyx ixyx]]]]]]]]]. move:(arg1_sr xy) (arg2_sr xy) => xE yE. move: (dl3 _ _ _ us xE vs). rewrite (inf_C r u x) (sup_C r u x) iu iv su sv. move: (least_greatest_pr or) => [p1 _ _ _];rewrite ! (p1 el _ (iE _ _ vs us)). move: (lattice_sup_pr lr xE us)(lattice_sup_pr lr xE vs)=> [_ h2 _][_ h3 _]. move: (lattice_sup_pr lr vs us) => [q1 q2 q3]. move: h2 h3; rewrite su sv; move=> h2 h3; move: (q3 _ h3 h2) => h4. rewrite (inf_C r y _) (inf_C r y _) ! (inf_comparable1 or h4) => infs. move: (lattice_inf_pr lr vs us); rewrite infs; move => [r1 r2 r3]. move: (order_transitivity or q1 r2)(order_transitivity or q2 r1) => h5 h6. order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)