fact: Fixpoint redivp_rec_loopT (q : polyF) sq cq (c : nat) (qq r : polyF) (n : nat) {struct n} : cps (nat * polyF * polyF) := 'let sr <- sizeT r; if sr < sq then ret (c, qq, r) else 'let lr <- lead_coefT r; let m := amulXnT lr (sr - sq) in let qq1 := sumpT (mulpT qq [::cq]) m in let r1 := sumpT (mulpT r ([::cq])) (opppT (mulpT m q)) in if n is n1.+1 then redivp_rec_loopT q sq cq c.+1 qq1 r1 n1 else ret (c.+1, qq1, r1).
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)