fact: Definition multiple_interpolation2 f x := let n := (BZ_val (BQfloor (BQinv x))) in Yo (n = \0c) (x +q (f \0c) -q \1q) (simple_interpolation2 n (f n) (f (cpred n)) x).
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)