proposition: Lemma near_swap {U V} (F : set_system U) (G : set_system V) (P : U -> set V) : (\forall x \near F & y \near G, P x y) = (\forall y \near G & x \near F, P x y).
proof: Proof. rewrite propeqE; split => -[[/=A B] [FA FB] ABP]; by exists (B, A) => // -[x y] [/=Bx Ay]; apply: (ABP (y, x)). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed