proposition: Lemma map_polyE p : map_poly p = Poly (map f p).
proof: Proof. rewrite /map_poly unlock; congr Poly. apply: (@eq_from_nth _ 0); rewrite size_mkseq ?size_map // => i lt_i_p. by rewrite [RHS](nth_map 0) ?nth_mkseq. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)