proposition: Lemma eval_ProdPoly e T s f k f' k' : (forall x k k', (forall p, (qf_eval e (k p) = k' (eval_poly e p))) -> qf_eval e (f x k) = k' (f' x)) -> (forall p, qf_eval e (k p) = k' (eval_poly e p)) -> qf_eval e (@ProdPoly _ T s f k) = k' (\prod_(x <- s) f' x).
proof: Proof. move=> Pf; elim: s k k'=> [|a s ihs] k k' Pk /=. by rewrite big_nil Pk /= !(mul0r, add0r). rewrite (Pf _ _ (fun fa => k' (fa * \prod_(x <- s) f' x))). by rewrite big_cons. move=> fa; rewrite (ihs _ (fun fs => k' (eval_poly e fa * fs))) //. by move=> fs; rewrite Pk eval_OpPoly. 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)