proposition: Lemma fct_ent_filter : Filter fct_ent.
proof: Proof. apply: filter_from_filter; first by exists setT; apply: filterT. move=> A B entA entB. exists (A `&` B); first exact: filterI. by move=> fg ABfg; split=> t; have [] := ABfg 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