proposition: Lemma rgcdpT_qf (p : polyF) (q : polyF) : rpoly p -> rpoly q -> qf_cps rpoly (rgcdpT p q).
proof: Proof. move=> rp rq k kP; rewrite /rgcdpT /=; do ![rewrite sizeT_qf => // ? _]. case: (_ < _); rewrite ?isnull_qf // => -[]; rewrite ?kP // => _; by rewrite sizeT_qf => // ? _; rewrite rgcdp_loopT_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)