proposition: Lemma eq_setSU (A B : {set T}) : A \subset B -> A :|: B = B.
proof: Proof. move=> HA; apply/setP=> y. rewrite !inE. case Hy: (y \in A) => //=. by rewrite (subsetP HA). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist