proposition: Lemma rgdcop_recT_qf (n : nat) (p : polyF) (q : polyF) : rpoly p -> rpoly q -> qf_cps rpoly (rgdcop_recT n p q).
proof: Proof. elim: n => [|n ihn] in p q * => k kP rp rq /=. by rewrite isnull_qf => //*; rewrite rq. rewrite rgcdpT_qf=> //*; rewrite sizeT_qf=> //*. case: (_ == _); rewrite ?kP ?rq //= redivpT_qf=> //= ? /andP[??]. by rewrite ihn. 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)