proposition: Lemma roots_mul a b : a < b -> forall p q, p != 0 -> q != 0 -> perm_eq (roots (p*q) a b) (roots p a b ++ roots ((gdcop p q)) a b).
proof: Proof. move=> hab p q np0 nq0. apply: uniq_perm; first exact: uniq_roots. rewrite cat_uniq ?uniq_roots andbT /=; apply/hasPn=> x /=. move/root_roots; rewrite root_gdco //; case/andP=> _. by rewrite in_roots !negb_and=> ->. move=> x; rewrite mem_cat !in_roots root_gdco //. rewrite rootM mulf_eq0 gdcop_eq0 negb_and. case: (x \in `]_, _[); last by rewrite !andbF. by rewrite negb_or !np0 !nq0 !andbT /=; do 2?case: root=> //=. 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)