proposition: Lemma rgcdpTsP (k : polyF -> fF) : (forall p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p)))) -> forall ps e, qf_eval e (rgcdpTs ps k) = qf_eval e (k (lift (\big[@rgcdp _/0%:P]_(i <- ps)(eval_poly e i)))).
proof: Proof. move=> Pk ps e; elim: ps k Pk => [|p ps Pps] /= k Pk. by rewrite /= big_nil Pk /= mul0r add0r. by rewrite big_cons Pps => *; rewrite !rgcdpTP // !eval_lift -?Pk. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice ssrnat seq) mathcomp(fintype generic_quotient bigop ssralg poly) mathcomp(polydiv matrix mxpoly countalg ring_quotient)