fact: Fixpoint toom_rec m p q : {poly R} := if m is m'.+1 then let: b := (maxn (divn (size p) n) (divn (size q) n)).+1 in let: sp := split_poly n b p in let: sq := split_poly n b q in let: ep := evaluate sp in let: eq := evaluate sq in let: r := \row_i (toom_rec m' (ep 0 i) (eq 0 i)) in let: w := interpolate r in w.['X^b] 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)