proposition: Lemma redivp_rec_loopT_qf (q : polyF) (sq : nat) (cq : tF) (c : nat) (qq r : polyF) (n : nat) : rpoly q -> rterm cq -> rpoly qq -> rpoly r -> qf_cps (fun x => [&& rpoly x.1.2 & rpoly x.2]) (redivp_rec_loopT q sq cq c qq r n).
proof: Proof. do ![move=>x/(pair x){x}] => rw; elim: n => [|n IHn]//= in q sq cq c qq r rw *; apply: qf_cps_bind; do ?[by apply: sizeT_qf; rewrite !rw] => sr _; case: ifPn => // _; do ?[by apply: qf_cps_ret; rewrite //= ?rw]; apply: qf_cps_bind; do ?[by apply: lead_coefT_qf; rewrite !rw] => lr /= rlr; [apply: qf_cps_ret|apply: IHn]; by do !rewrite ?(rsumpT,rmulpT,ramulXnT,rpoly_map_mul,rlr,rw) //=. 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)