proposition: Lemma rgdcopT_qf (p : polyF) (q : polyF) : rpoly p -> rpoly q -> qf_cps rpoly (rgdcopT p q).
proof: Proof. by move=> rp rq k kP; rewrite sizeT_qf => //*; rewrite rgdcop_recT_qf. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice ssrnat seq) mathcomp(fintype generic_quotient bigop ssralg poly) mathcomp(polydiv matrix mxpoly countalg ring_quotient)