proposition: Lemma prod_ent_split A : prod_ent A -> exists2 B, prod_ent B & B \; B `<=` A.
proof: Proof. move=> [B [entB1 entB2]] sBA; exists [set xy | split_ent B.1 (xy.1.1,xy.2.1) /\ split_ent B.2 (xy.1.2,xy.2.2)]. by apply: prod_entP; apply: entourage_split_ent. move=> xy [uv /= [hB1xyuv1 hB2xyuv1] [hB1xyuv2 hB2xyuv2]]. have /sBA : (B.1 `*` B.2) ((xy.1.1, xy.2.1),(xy.1.2,xy.2.2)). by split=> /=; apply: subset_split_ent => //; [exists uv.1|exists uv.2]. move=> [zt Azt /eqP]; rewrite !xpair_eqE andbACA -!xpair_eqE. by rewrite -!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