proposition: Lemma ex_elim_seq_qf (ps : seq polyF) (q : polyF) : all rpoly ps -> rpoly q -> qf (ex_elim_seq ps q).
proof: Proof. move=> rps rq; apply: rgcdpTs_qf=> // g rg; apply: rgdcopT_qf=> // d rd. exact : sizeT_qf. 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)