proposition: Lemma roots_eq (p q : {poly R}) (a b : R) : p != 0 -> q != 0 -> ({in `]a, b[, root p =1 root q} <-> roots p a b = roots q a b).
proof: Proof. move=> p0 q0; split=> hpq; last first. by move=> x hx; rewrite !(root_is_roots _ hx) // hpq. apply: (@roots_on_uniq p a b); rewrite ?path_roots //. exact: roots_on_roots. move=> x; case hx: (_ \in _). by rewrite -hx hpq //; apply: roots_on_roots. by rewrite /= -(andFb (q.[x] == 0)) -hx; apply: roots_on_roots. 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)