proposition: Lemma setI_inf s E: sub s (\Po E) -> greatest_lower_bound (subp_order E) s (Yo (nonempty s) (intersection s) E).
proof: Proof. move=> sp. have [oi si1] := (subp_osr E). have nee: ~ nonempty emptyset by move/nonemptyP. case: (emptyset_dichot s)=> h. by rewrite h Y_false // glb_set0 //; apply: wholeset_greatest. Ytac0. have si: sub (intersection s) E by apply:setI_sub2 => i/sp /setP_P. have ss: sub s (substrate (subp_order E)) by rewrite si1. apply/(glbP oi ss); rewrite /lower_bound si1; split. split; first by apply/setP_P. move=> y ys; apply /subp_gleP; split => //. by apply/setP_P; apply: sp. by apply: setI_s1. move=> z [] /setP_P zE hyp. apply /subp_gleP; split => // t tz. by apply: (setI_i h) => y /hyp /subp_gleP [_ _]; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)