proposition: Lemma eval_TaqsR e p sq i k k' : (forall x, qf_eval e (k x) = k' (eval e x)) -> qf_eval e (TaqsR p sq i k) = k' (taqsR (eval_poly e p) (map (eval_poly e) sq) i).
proof: Proof. by move=> Pk; rewrite /TaqsR /taqsR eval_TaqR Pk /= eval_Pcq. 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)