proposition: Lemma prod_ent_refl A : prod_ent A -> [set xy | xy.1 = xy.2] `<=` A.
proof: Proof. move=> [B [entB1 entB2] sBA] xy /eqP. rewrite [_.1]surjective_pairing [xy.2]surjective_pairing xpair_eqE. move=> /andP [/eqP xy1e /eqP xy2e]. have /sBA : (B.1 `*` B.2) ((xy.1.1, xy.2.1), (xy.1.2, xy.2.2)). by rewrite xy1e xy2e; split=> /=; apply: entourage_refl. move=> [zt Azt /eqP]; rewrite !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