proposition: Lemma eval_SeqMInfty e ps k k' : (forall xs, qf_eval e (k xs) = k' (map (eval e) xs)) -> qf_eval e (SeqMInfty ps k) = k' (map (fun p : {poly F} => (-1) ^+ (~~ odd (size p)) * lead_coef p) (map (eval_poly e) ps)).
proof: Proof. elim: ps k k' => [|p ps ihps] k k' Pk /=; first by rewrite Pk. set X := lead_coef _; grab_eq k'' X; apply: eval_LeadCoef => lp {X}. rewrite eval_Size /= /k'' {k''}. by set X := map _ _; grab_eq k'' X; apply: ihps => {X} lps; rewrite Pk. 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)