proposition: Lemma eval_BigRgcd e ps k k' : (forall p, qf_eval e (k p) = k' (eval_poly e p)) -> qf_eval e (BigRgcd ps k) = k' (\big[@rgcdp _/0%:P]_(i <- ps) (eval_poly e i)).
proof: Proof. elim: ps k k'=> [|p sp ihsp] k k' Pk /=. by rewrite big_nil Pk /= mul0r add0r. rewrite big_cons (ihsp _ (fun r => k' (rgcdp (eval_poly e p) r))) //. by move=> r; apply: eval_Rgcd. 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)