proposition: Lemma prod_ent_filter : Filter prod_ent.
proof: Proof. have prodF := filter_prod_filter (@entourage_pfilter U) (@entourage_pfilter V). split; rewrite /prod_ent; last 1 first. - by move=> A B sAB /=; apply: filterS => ? [xy /sAB ??]; exists xy. - by rewrite -setMTT; apply: prod_entP filterT filterT. move=> A B /= entA entB; apply: filterS (filterI entA entB) => xy []. move=> [zt Azt ztexy] [zt' Bzt' zt'exy]; exists zt => //; split=> //. move/eqP: ztexy; rewrite -zt'exy !xpair_eqE. by rewrite andbACA -!xpair_eqE -!surjective_pairing => /eqP->. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed