proposition: Lemma eval_Rgcd_loop e n p q k k' : (forall p, qf_eval e (k p) = k' (eval_poly e p)) -> qf_eval e (Rgcd_loop n p q k) = k' (rgcdp_loop n (eval_poly e p) (eval_poly e q)).
proof: Proof. elim: n p q k k'=> [|n ihn] p q k k' Pk /=. rewrite (eval_Rediv (fun r => if r.2%PAIR == 0 then k' (eval_poly e q) else k' r.2%PAIR)) /=. by case: eqP. by move=> _ _ r; rewrite eval_Isnull; case: eqP. pose q' := eval_poly e q. rewrite (eval_Rediv (fun r => if r.2%PAIR == 0 then k' q' else k' (rgcdp_loop n q' r.2%PAIR))) /=. by case: eqP. move=> _ _ r; rewrite eval_Isnull; case: eqP; first by rewrite Pk. by rewrite (ihn _ _ _ k'). 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)