proposition: Lemma rseq_poly_map (x : nat) (ts : seq tF) : all (@rterm _) ts -> all rpoly (map (abstrX x) ts).
proof: Proof. by elim: ts => //= t ts iht; case/andP=> rt rts; rewrite rabstrX // 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)