proposition: Lemma toom_cookE p q : toom_cook p q = p * q.
proof: Proof. rewrite /toom_cook; case: (ltnP 0 n)=> // hn0; exact: toom_recE. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div fintype tuple) mathcomp(finfun bigop fingroup perm ssralg zmodp matrix mxalgebra) mathcomp(poly polydiv mxpoly)