proposition: Lemma holds_ex_elim: GRing.valid_QE_proj ex_elim.
proof: Proof. move=> i [ps qs] /= e; case/andP=> /= rps rqs. rewrite ex_elim_seqP big_map. have -> : \big[@rgcdp _/0%:P]_(j <- ps) eval_poly e (abstrX i j) = \big[@rgcdp _/0%:P]_(j <- (map (eval_poly e) (map (abstrX i) (ps)))) j. by rewrite !big_map. rewrite -!map_comp. have aux I (l : seq I) (P : I -> {poly F}) : \big[(@gcdp F)/0]_(j <- l) P j %= \big[(@rgcdp F)/0]_(j <- l) P j. elim: l => [| u l ihl] /=; first by rewrite !big_nil eqpxx. rewrite !big_cons; move: ihl; move/(eqp_gcdr (P u)) => h. by apply: eqp_trans h _; rewrite eqp_sym; apply: eqp_rgcd_gcd. case g0: (\big[(@rgcdp F)/0%:P]_(j <- map (eval_poly e \o abstrX i) ps) j == 0). rewrite (eqP g0) rgdcop0. case m0 : (_ == 0)=> //=; rewrite ?(size_poly1,size_poly0) //=. rewrite abstrX_bigmul eval_bigmul -bigmap_id in m0. constructor=> [[x] // []] //. case=> _; move/holds_conjn=> hc; move/hc:rqs. by rewrite -root_bigmul //= (eqP m0) root0. constructor; move/negP:m0; move/negP=>m0. case: (closed_nonrootP F_closed _ m0) => x {m0}. rewrite abstrX_bigmul eval_bigmul -bigmap_id root_bigmul=> m0. exists x; do 2?constructor=> //; last by apply/holds_conjn. apply/holds_conj; rewrite //= -root_biggcd. by rewrite (eqp_root (aux _ _ _ )) (eqP g0) root0. apply: (iffP (closed_rootP F_closed _)) => -[x Px]; exists x; move: Px => //=. rewrite (eqp_root (@eqp_rgdco_gdco F _ _)) root_gdco ?g0 //. rewrite -(eqp_root (aux _ _ _ )) root_biggcd abstrX_bigmul eval_bigmul. rewrite -bigmap_id root_bigmul; case/andP=> psr qsr. do 2?constructor; first by apply/holds_conj. by apply/holds_conjn. rewrite (eqp_root(@eqp_rgdco_gdco F _ _)) root_gdco?g0// -(eqp_root(aux _ _ _)). rewrite root_biggcd abstrX_bigmul eval_bigmul -bigmap_id. rewrite root_bigmul=> [[] // [hps hqs]]; apply/andP. constructor; first by apply/holds_conj. by apply/holds_conjn. 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)