proposition: Lemma roots_on_same s' p i s : s =i s' -> (roots_on p i s <-> roots_on p i s').
proof: Proof. by move=> hss'; split=> hs x; rewrite (hss', (I, hss')). 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)