proposition: Lemma near_pair {T U} {F : set_system T} {G : set_system U} {FF : Filter F} {FG : Filter G} (P : in_filter F) (Q : in_filter G) x : prop_of P x.1 -> prop_of Q x.2 -> prop_of (in_filter_prod P Q) x.
proof: Proof. by case: x=> x y; do ?rewrite prop_ofE /=; split. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed