proposition: Lemma meets_globallyl T (A : set T) G : globally A `#` G = forall B, G B -> A `&` B !=set0.
proof: Proof. rewrite propeqE; split => [/(_ _ _ (fun=> id))//|clA A' B sA]. by move=> /clA; apply: subsetI_neq0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed