proposition: Lemma prod_ent_nbhsE : nbhs = nbhs_ prod_ent.
proof: Proof. rewrite predeq2E => xy A; split=> [[B []] | [B [C [entC1 entC2] sCB] sBA]]. rewrite -!nbhs_entourageE => - [C1 entC1 sCB1] [C2 entC2 sCB2] sBA. exists [set xy | C1 (xy.1.1, xy.2.1) /\ C2 (xy.1.2, xy.2.2)]. exact: prod_entP. by move=> uv [/= /sCB1 Buv1 /sCB2 /(conj Buv1) /sBA]. exists (to_set (C.1) (xy.1), to_set (C.2) (xy.2)). by rewrite -!nbhs_entourageE; split; [exists C.1|exists C.2]. move=> uv [/= Cxyuv1 Cxyuv2]; apply: sBA. have /sCB : (C.1 `*` C.2) ((xy.1,uv.1),(xy.2,uv.2)) by []. move=> [zt Bzt /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