proposition: Lemma prod_nbhs_filter (p : T * U) : ProperFilter (prod_nbhs p).
proof: Proof. exact: filter_prod_proper. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed