fact: Definition ex_elim_seq (ps : seq polyF) (q : polyF) : fF := ('let g <- rgcdpTs ps; 'let d <- rgdcopT q g; 'let n <- sizeT d; ret (n != 1)) GRing.Bool.
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)