fact: Definition redivp_rec (q : {poly R}) := let sq := size q in let cq := lead_coef q in fix loop (k : nat) (qq r : {poly R})(n : nat) {struct n} := if size r < sq 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 loop k.+1 qq1 r1 n1 else (k.+1, qq1, r1).
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)