proposition: Lemma map_monic p : (p^f \is monic) = (p \is monic).
proof: Proof. by rewrite [in LHS]monicE lead_coef_map fmorph_eq1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)