proposition: Lemma eq_map_poly (g : aR -> rR) : f =1 g -> map_poly f =1 map_poly g.
proof: Proof. by move=> eq_fg p; rewrite !map_polyE (eq_map eq_fg). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)