proposition: Lemma rgcdp_loopT_qf (n : nat) (p : polyF) (q : polyF) : rpoly p -> rpoly q -> qf_cps rpoly (rgcdp_loopT n p q).
proof: Proof. elim: n => [|n IHn] in p q * => rp rq /=; (apply: qf_cps_bind=> [|rr rrr]; [ apply: qf_cps_bind => [|[[a u] v]]; do ?exact: redivpT_qf; by move=> /andP[/= ??]; apply: (@qf_cps_ret _ rpoly)| apply: qf_cps_bind => [|[] _]; by [apply: isnull_qf|apply: qf_cps_ret|apply: 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)