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