proposition: Lemma roots_mul_coprime a b : a < b -> forall p q, p != 0 -> q != 0 -> coprimep p q -> perm_eq (roots (p * q) a b) (roots p a b ++ roots q a b).
proof: Proof. move=> hab p q np0 nq0 cpq. rewrite (perm_trans (roots_mul hab np0 nq0)) //. suff ->: roots (gdcop p q) a b = roots q a b by apply: perm_refl. case: gdcopP=> r rq hrp /(_ q (dvdpp _)). rewrite coprimep_sym; move/(_ cpq)=> qr. have erq : r %= q by rewrite /eqp rq qr. apply/roots_eq=> // [|x hx]; last exact: eqp_root. by rewrite -size_poly_eq0 (eqp_size erq) size_poly_eq0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg poly polydiv ssrnum zmodp) mathcomp(polyorder path interval ssrint)