fact: Fixpoint redivp_rec_loop (q : {poly F}) sq cq (k : nat) (qq r : {poly F})(n : nat) {struct n} := if (size r < sq)%N then (k, qq, r) else let m := (lead_coef r) *: 'X^(size r - sq) in let qq1 := qq * cq%:P + m in let r1 := r * cq%:P - m * q in if n is n1.+1 then redivp_rec_loop q sq cq k.+1 qq1 r1 n1 else (k.+1, qq1, r1).
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(finfun path matrix) mathcomp(bigop order ssralg poly polydiv ssrnum zmodp div ssrint) mathcomp(polyorder polyrcf interval polyXY) mathcomp(qe_rcf_th ordered_qelim mxtens)