proposition: Lemma map_diff_roots x y : diff_roots (f x) (f y) = (x != y).
proof: Proof. rewrite /diff_roots -rmorphB // fmorph_unit // subr_eq0 //. by rewrite rmorph_comm // eqxx eq_sym. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)