proposition: Lemma eval_ChangesPoly e ps k : qf_eval e (ChangesPoly ps k) = qf_eval e (k (changes_poly (map (eval_poly e) ps))).
proof: Proof. rewrite (eval_SeqMInfty (fun mps => qf_eval e (k ((changes mps)%:Z - (changes_pinfty [seq eval_poly e i | i <- ps])%:Z)))) => // mps. rewrite (eval_SeqPInfty (fun pps => qf_eval e (k ((changes (map (eval e) mps))%:Z - (changes pps)%:Z)))) => // pps. by rewrite !eval_Changes. 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)