proposition: Lemma fct_ent_split A : fct_ent A -> exists2 B, fct_ent B & B \; B `<=` A.
proof: Proof. move=> [B entB sBA]. exists [set fg | forall t, split_ent B (fg.1 t, fg.2 t)]. by exists (split_ent B). move=> fg [h spBfh spBhg]. by apply: sBA => t; apply: entourage_split (spBfh t) (spBhg t). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed