proposition: Lemma edivp_map a b : edivp a^f b^f = (0, (a %/ b)^f, (a %% b)^f).
proof: Proof. have [-> | bn0] := eqVneq b 0. rewrite (rmorph0 (map_poly f)) WeakIdomain.edivp_def !modp0 !divp0. by rewrite (rmorph0 (map_poly f)) scalp0. rewrite unlock redivp_map lead_coef_map rmorph_unit; last first. by rewrite unitfE lead_coef_eq0. rewrite modpE divpE !map_polyZ [in RHS]rmorphV ?rmorphXn // unitfE. by rewrite expf_neq0 // lead_coef_eq0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)