proposition: Lemma Exercise1_17c A: boolean_lattice (subp_order A) /\ (forall x, inc x (\Po A) -> standard_completion (subp_order A) x = A -s x).
proof: Proof. move: (subp_osr A) => [];set (r:=subp_order A) => or sr. have ha:= setP_0i A. have lee: (least r emptyset). split; first by rewrite sr. move=> x; rewrite /r sr => h; apply /sub_gleP;split;fprops. have el: has_least r by exists emptyset. have thel: (the_least r = emptyset) by apply: the_least_pr2. move: (setP_Ti A) => hh. have geA: (greatest r A). red; rewrite sr /r; split => // s sp. apply /sub_gleP;split => //; apply /setP_P => //. have eg: has_greatest r by exists A. have theg: (the_greatest r = A) by apply: the_greatest_pr2. move: (sup_inclusion (A:=A)) => les. move: (inf_inclusion (A:=A)) => ges. have lr: lattice r by apply: setP_lattice. have le1: (forall x y, inc x (\Po A) -> inc y (\Po A) -> sup r x y = x \cup y). move=> x y /setP_P xA /setP_P yA; symmetry. by apply: (supremum_pr2 or); apply: les. have ge1: (forall x y, inc x (\Po A) ->inc y (\Po A) -> inf r x y = x \cap y). move=> x y /setP_P xA /setP_P yA; symmetry. by apply: (infimum_pr2 or); apply: ges. have rc: forall x y, sub x y -> sub y A -> [/\ inc (y -s x) (substrate r), sup r x (y -s x) = y & inf r x (y -s x) = the_least r]. move=> x y xy yA. have xA:inc x (\Po A) by apply /setP_P;apply: sub_trans yA. have cA: inc (y -s x) (\Po A). by apply /setP_P; move=> t /setC_P [ty _]; apply: yA. rewrite sr le1 // ge1 // thel; split;fprops. move /setI2id_Pr: xy => {1} <-; exact: setI2_Cr. by apply /set0_P => t /setI2_P [tx] /setC_P [_] ntx. have iuA: forall x y, inc x (\Po A) -> inc y (\Po A) -> (inc (x \cup y) (\Po A) /\ inc (x \cap y) (\Po A)). move => x y /setP_P xa /setP_P ya; split; apply/setP_P => t. by case/setU2_P; fprops. move /setI2_P => [tx ty]; fprops. have dl3: (distributive_lattice3 r). apply /(distributive_lattice_prop3 lr). move=> x y z; rewrite sr => xA yA zA. move:(proj2 (iuA _ _ yA zA)) (proj1 (iuA _ _ xA yA)) => iyzA uxyA. rewrite (ge1 _ _ yA zA) (le1 _ _ xA yA) (le1 _ _ xA iyzA) (ge1 _ _ zA uxyA). apply /sub_gleP. split; [ apply (proj2(iuA _ _ zA uxyA)) | apply (proj1(iuA _ _ xA iyzA)) |]. move=> t /setI2_P [tz]; case/setU2_P => tx; first by apply /setU2_P; left. by apply /setU2_P; right; fprops. have rc1:relatively_complemented r. split => //; move=> x y /sub_gleP [xA yA xy]. by exists (y -s x); apply: rc => //; apply /setP_P. have bl: boolean_lattice r by split => //. split => // x xa; move : (xa) => /setP_P xA. have sAA: sub A A by fprops. symmetry;apply: scompl_unique =>//; try ue. by red; rewrite theg; apply: rc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)