proposition: Lemma rpoly_map_mul (t : tF) (p : polyF) (rt : rterm t) : rpoly [seq (t * x)%T | x <- p] = rpoly p.
proof: Proof. by rewrite /rpoly all_map; apply/eq_all => x; rewrite /= rt. 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)