proposition: Lemma trivIset_out : trivIset C -> [disjoint x & cover C] -> trivIset (x |: C).
proof: Proof. move/trivIsetP => HC. rewrite disjoints_subset => Hx. apply/trivIsetP => A B HA HB HAB. rewrite !inE in HA HB. wlog: A B HAB HA HB / A == x. move/orP: (HA) => [] HA' //. by apply. move/orP: (HB) => [] HB' //. rewrite -setI_eq0 setIC setI_eq0. apply => //. by rewrite eq_sym. by move=> _; apply HC. move=> /eqP {}HA. move/orP: HB => [/eqP|] HB. by rewrite HA HB eqxx in HAB. rewrite HA disjoints_subset. apply (subset_trans Hx). by rewrite subsetC setCK bigcup_sup. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist