fact: Definition Npoly (R : comRingType) : nat -> comRingType := fix aux n := if n is n.+1 then poly_comRingType (aux n) else R.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq ssralg ssrint) mathcomp(path choice fintype tuple finset ssralg bigop poly polydiv) mathcomp(zmodp) CoqEAL(hrel param refinements binint poly_op hpoly karatsuba)