fact: Definition toom_cook (p q : {poly R}) := if 0 < n then toom_rec (maxn (size p) (size q)) p q else p * q.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div fintype tuple) mathcomp(finfun bigop fingroup perm ssralg zmodp matrix mxalgebra) mathcomp(poly polydiv mxpoly)