proposition: Lemma set_flatten_cond (P1 P2 : pred T) : [set x in [set x | P1 x] | P2 x] = [set x | P1 x & P2 x].
proof: Proof. by apply/setP => x; rewrite !inE. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist