proposition: Lemma monic_map_inj (aR rR : ringType) (f : aR -> rR) (p : {poly aR}) : injective f -> f 0 = 0 -> f 1 = 1 -> map_poly f p \is monic = (p \is monic).
proof: Proof. move=> inj_f eq_f00 eq_f11; rewrite !monicE lead_coef_map_inj ?rmorph0 //. by rewrite -eq_f11 inj_eq. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype finfun perm matrix bigop zmodp mxalgebra) mathcomp(choice poly polydiv mxpoly binomial)