proposition: Lemma ex_elim_seqP (ps : seq polyF) (q : polyF) (e : seq F) : let gp := (\big[@rgcdp _/0%:P]_(p <- ps)(eval_poly e p)) in qf_eval e (ex_elim_seq ps q) = (size (rgdcop (eval_poly e q) gp) != 1).
proof: Proof. by do ![rewrite (rgcdpTsP,rgdcopTP,sizeTP,eval_lift) //= | move=> * //=]. 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)