proposition: Lemma Exercise1_17d r x y: boolean_lattice r -> inc x (substrate r) -> inc y (substrate r) -> let ys := (standard_completion r y) in [/\ inf r y (sup r ys x) = inf r y x, sup r y (inf r ys x) = sup r y x, inf r ys (sup r y x) = inf r ys x & sup r ys (inf r y x) = sup r ys x].
proof: Proof. move=> blr xsr ysr ys. move: (blr) => [[lr _ _] _ dl3]; move: (lr) => [or _]. move: (scompl_pr blr ysr); rewrite -/ys; move=> [ys1 ys2 ys3]. move: (distributive_lattice_prop2 lr) => [_ ok1 ok2]. rewrite ((ok1 dl3) _ _ _ ysr ys1 xsr) ((ok1 dl3) _ _ _ ys1 ysr xsr). rewrite ((ok2 dl3) _ _ _ ysr ys1 xsr) ((ok2 dl3) _ _ _ ys1 ysr xsr). rewrite (sup_C r ys y) (inf_C r ys y) ys2 ys3. move:(lattice_props lr) =>/=; move => [sE [iE _]]; split. by case: (least_greatest_pr1 blr (iE _ _ ysr xsr)). by rewrite inf_C;move: (least_greatest_pr1 blr (sE _ _ ysr xsr))=> [_ ]. by case: (least_greatest_pr1 blr (iE _ _ ys1 xsr)). by rewrite inf_C;move: (least_greatest_pr1 blr (sE _ _ ys1 xsr)) => [_]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)