proposition: Lemma separable_prod_XsubC (r : seq R) : separable (\prod_(x <- r) ('X - x%:P)) = uniq r.
proof: Proof. elim: r => [|x r IH]; first by rewrite big_nil unlock /separable_poly coprime1p. by rewrite big_cons mulrC separable_root IH root_prod_XsubC andbC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop finset prime) mathcomp(binomial ssralg poly polydiv fingroup perm) mathcomp(morphism quotient gproduct finalg zmodp cyclic) mathcomp(matrix mxalgebra mxpoly polyXY vector falgebra) mathcomp(fieldext)