fact: Fixpoint karatsuba_rec (n : nat) (p q : {poly R}) := if n is n'.+1 then let np := normalize p in let nq := normalize q in let sp := size p in let sq := size q in if (sp <= 2) || (sq <= 2) then p * q else let m := minn sp./2 sq./2 in let (p1,p2) := split_poly m p in let (q1,q2) := split_poly m q in let p1q1 := karatsuba_rec n' p1 q1 in let p2q2 := karatsuba_rec n' p2 q2 in let p12 := p1 + p2 in let q12 := q1 + q2 in let p12q12 := karatsuba_rec n' p12 q12 in shift_poly (2 * m)%N p1q1 + shift_poly m (p12q12 - p1q1 - p2q2) + p2q2 else p * q.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(zmodp path choice fintype tuple finset ssralg) mathcomp(bigop poly polydiv)