proposition: Lemma prod_XsubC_eq (s t : seq L) : \prod_(x <- s) ('X - x%:P) = \prod_(x <- t) ('X - x%:P) -> perm_eq s t.
proof: Proof. move=> eq_prod; apply/allP => x _ /=; apply/eqP. by have /(congr1 (mup x)) := eq_prod; rewrite !mu_prod_XsubC. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)