fact: Fixpoint sumpT (p q : polyF) := match p, q with a :: p, b :: q => (a + b)%T :: sumpT p q | [::], q => q | p, [::] => p end.
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)