fact: Fixpoint karatsuba_rec n (p q : polyA) := match n with | 0 => (p * q)%C | n'.+1 => let sp := sizep p in let sq := sizep q in if (sp <= 1 + 1)%C || (sq <= 1 + 1)%C then (p * q)%C else let m := implem (minn (spec sp)./2 (spec sq)./2) in let (p1,p2) := splitp m p in let (q1,q2) := splitp m q in let p1q1 := karatsuba_rec n' p1 q1 in let p2q2 := karatsuba_rec n' p2 q2 in let p12 := (p1 + p2)%C in let q12 := (q1 + q2)%C in let p12q12 := karatsuba_rec n' p12 q12 in (shiftp ((1 + 1) * m)%C p1q1 + shiftp m (p12q12 - p1q1 - p2q2) + p2q2)%C end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq ssralg) mathcomp(path choice fintype tuple finset bigop poly polydiv) CoqEAL(hrel param refinements poly_op)