proposition: Lemma eval_TaqR e p q k : qf_eval e (TaqR p q k) = qf_eval e (k (taqR (eval_poly e p) (eval_poly e q))).
proof: Proof. rewrite (eval_Mods (fun r => qf_eval e (k (changes_poly r)))). by rewrite !eval_OpPoly. by move=> sp; rewrite !eval_ChangesPoly. 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)