proposition: Lemma eval_Rediv e p q k k' (d := (redivp (eval_poly e p) (eval_poly e q))) : (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 p q k) = k' d.
proof: Proof. move=> Pk; rewrite eval_Isnull /d unlock. have [_|p_neq0] /= := boolP (_ == _); first by rewrite Pk /= mul0r add0r. rewrite !eval_Size; set p' := eval_poly e p; set q' := eval_poly e q. rewrite (eval_LeadCoef (fun lq => k' (redivp_rec_loop q' (size q') lq 0 0 p' (size p')))) /=; last first. by move=> x; rewrite (eval_Rediv_rec_loop k') //= mul0r add0r. by rewrite redivp_rec_loopP. 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)