fact: Definition karatsuba p q := karatsuba_rec (maxn (spec (sizep p)) (spec (sizep q))) p q.
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)