proposition: Lemma scompl_mon r x y: boolean_lattice r -> gle r x y -> gle r (standard_completion r y) (standard_completion r x).
proof: Proof. move=> blr xy. move: (arg1_sr xy) (arg2_sr xy) => xE yE. move: (scompl_pr blr xE) (scompl_pr blr yE). move=> [aE supa infa] [bE supb infb]. move: (blr) => [[lr _ _] eg dl3];move: (lr) => [or _]. move:(lattice_props lr). set (E:= substrate r). move => [sE [iE [sixy [isxy [sxyz [ixyz [sxx [ixx [sxyx ixyx]]]]]]]]]. set (a:= standard_completion r x). set (b:= standard_completion r y). set (c := inf r a b). have iyc: (inf r y c = the_least r). rewrite /c (inf_C r a b) (ixyz _ _ _ yE bE aE) infb. by move: (least_greatest_pr1 blr aE)=> [_ _ ok _]. move: (sE _ _ yE aE) => yaE. have syc: sup r y c = sup r y a. rewrite/c (proj32 (distributive_lattice_prop2 lr)) //. rewrite supb;exact: (proj42 (least_greatest_pr1 blr yaE)). move: (proj2 (the_greatest_pr or eg) _ yaE)=> le1. have : (gle r (sup r x a) (sup r y a)). by rewrite sup_C (sup_C r y a); apply: sup_monotone. rewrite supa => le2; rewrite (order_antisymmetry or le1 le2) in syc. move: (iE _ _ aE bE) => cE. have yc: c = standard_completion r y by apply: scompl_unique. move: (lattice_inf_pr lr aE bE) => [ac _ _]; rewrite -/c yc in ac; exact ac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)