proposition: Lemma rmulpT (p q : polyF) : rpoly p -> rpoly q -> rpoly (mulpT p q).
proof: Proof. elim: p q=> [|a p ihp] q rp rq //=; move: rp; case/andP=> ra rp /=. apply: rsumpT; last exact: ihp. by rewrite rpoly_map_mul. 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)