proposition: Lemma eval_Rediv_rec_loop e q sq cq c qq r n k k' (d := redivp_rec_loop (eval_poly e q) sq (eval e cq) c (eval_poly e qq) (eval_poly e r) n) : (forall c qq r, qf_eval e (k (c, qq, r)) = k' (c, eval_poly e qq, eval_poly e r)) -> qf_eval e (Rediv_rec_loop q sq cq c qq r n k) = k' d.
proof: Proof. move=> Pk; elim: n c qq r k Pk @d=> [|n ihn] c qq r k Pk /=. rewrite eval_Size /=; have [//=|gtq] := ltnP. set X := lead_coef _; grab_eq k'' X; apply: eval_LeadCoef => {X}. by move=> x /=; rewrite Pk /= !eval_OpPoly /= !mul_polyC. rewrite eval_Size /=; have [//=|gtq] := ltnP. set X := lead_coef _; grab_eq k'' X; apply: eval_LeadCoef => {X}. by move=> x; rewrite ihn // !eval_OpPoly /= !mul_polyC. 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)