proposition: Lemma near2_pair {U V} (F : set_system U) (G : set_system V) (P : set (U * V)) : {near F & G, forall x y, P (x, y)} = {near (F, G), forall x, P x}.
proof: Proof. by symmetry; congr (nbhs _); rewrite predeqE => -[]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed