proposition: Lemma redivpT_qf (p : polyF) (q : polyF) : rpoly p -> rpoly q -> qf_cps (fun x => [&& rpoly x.1.2 & rpoly x.2]) (redivpT p q).
proof: Proof. move=> rp rq; apply: qf_cps_bind => [|[] _]; first exact: isnull_qf. by apply: qf_cps_ret. apply: qf_cps_bind => [|sp _]; first exact: sizeT_qf. apply: qf_cps_bind => [|sq _]; first exact: sizeT_qf. apply: qf_cps_bind => [|lq rlq]; first exact: lead_coefT_qf. by apply: redivp_rec_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)