proposition: Lemma redivp_map a b : redivp a^f b^f = (rscalp a b, (rdivp a b)^f, (rmodp a b)^f).
proof: Proof. rewrite /rdivp /rscalp /rmodp !unlock map_poly_eq0 size_map_poly. have [// | q_nz] := ifPn; rewrite -(rmorph0 (map_poly f)) //. have [m _] := ubnPeq (size a); elim: m 0%N 0 a => [|m IHm] qq r a /=. rewrite -!mul_polyC !size_map_poly !lead_coef_map // -(map_polyXn f). by rewrite -!(map_polyC f) -!rmorphM -rmorphB -rmorphD; case: (_ < _). rewrite -!mul_polyC !size_map_poly !lead_coef_map // -(map_polyXn f). by rewrite -!(map_polyC f) -!rmorphM -rmorphB -rmorphD /= IHm; case: (_ < _). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)