proposition: Lemma ex_elim_qf (x : nat) (pqs : seq tF * seq tF) : GRing.dnf_rterm pqs -> qf (ex_elim x pqs).
proof: Proof. case: pqs => ps qs; case/andP=> /= rps rqs. apply: ex_elim_seq_qf; first exact: rseq_poly_map. apply: rabstrX=> /=. elim: qs rqs=> [|t ts iht] //=; first by rewrite big_nil. by case/andP=> rt rts; rewrite big_cons /= rt /= iht. 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)