proposition: Lemma prod_ent_inv A : prod_ent A -> prod_ent (A^-1)%classic.
proof: Proof. move=> [B [/entourage_inv entB1 /entourage_inv entB2] sBA]. have:= prod_entP entB1 entB2; rewrite /prod_ent/=; apply: filterS. move=> _ [p /(sBA (_,_)) [[x y] ? xyE] <-]; exists (y,x) => //; move/eqP: xyE. by rewrite !xpair_eqE => /andP[/andP[/eqP-> /eqP->] /andP[/eqP-> /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