proposition: Lemma toom_recE (Hn0 : 0 < n) : forall m p q, toom_rec m p q = p * q.
proof: Proof. elim=> //= m ih p q. set sp := split_poly _ _ p; set sq := split_poly _ _ q. set ep := evaluate sp; set eq := evaluate sq. have hspq : size (sp * sq) <= d. rewrite (leq_trans (size_mul_leq _ _)) // /d -!subn1 leq_sub2r // -addnn. by apply/leq_add; rewrite size_poly. have -> : \row_i toom_rec m (ep 0 i) (eq 0 i) = \row_i (sp * sq).[points`_i]. by apply/rowP=> i; rewrite mxE ih /ep /eq !evaluateE !mxE hornerM. by rewrite (interpolateE hspq) hornerM !recompose_split ?basisE // maxnC basisE. 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)