proposition: Lemma redivp_rec_loopP q c qq r n : redivp_rec q c qq r n = redivp_rec_loop q (size q) (lead_coef q) c qq r n.
proof: Proof. by elim: n c qq r => [| n Pn] c qq r //=; rewrite Pn. Qed.
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)