proposition: Lemma egcdp_map p q : egcdp (map_poly f p) (map_poly f q) = (map_poly f (egcdp p q).1, map_poly f (egcdp p q).2).
proof: Proof. wlog le_qp: p q / size q <= size p. move=> IH; have [/IH// | lt_qp] := leqP (size q) (size p). have /IH := ltnW lt_qp; rewrite /egcdp !size_map_poly ltnW // leqNgt lt_qp /=. by case: (egcdp_rec _ _ _) => u v [-> ->]. rewrite /egcdp !size_map_poly {}le_qp; move: (size q) => n. elim: n => /= [|n IHn] in p q *; first by rewrite rmorph1 rmorph0. rewrite map_poly_eq0; have [_ | nz_q] := ifPn; first by rewrite rmorph1 rmorph0. rewrite -map_modp (IHn q (p %% q)); case: (egcdp_rec _ _ n) => u v /=. rewrite map_polyZ lead_coef_map -rmorphXn scalp_map rmorphB rmorphM. by rewrite -map_divp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)