proposition: Lemma gdcop_rec_map p q n : (gdcop_rec p q n)^f = gdcop_rec p^f q^f n.
proof: Proof. elim: n p q => [|n IH] => /= p q. by rewrite map_poly_eq0; case: eqP; rewrite ?rmorph1 ?rmorph0. rewrite /coprimep -gcdp_map size_map_poly. by case: eqP => Hq0 //; rewrite -map_divp -IH. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)