proposition: Lemma redivp_rec_loopP (q : {poly F}) (c : nat) (qq r : {poly F}) (n : nat) : 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: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice ssrnat seq) mathcomp(fintype generic_quotient bigop ssralg poly) mathcomp(polydiv matrix mxpoly countalg ring_quotient)