fact: Fixpoint amulXnT (a : tF) (n : nat) : polyF := if n is n'.+1 then 0%T :: (amulXnT a n') else [:: a].
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)