fact: Definition sum_f (s n:nat) (f:nat -> R) : R := sum_f_R0 (fun x:nat => f (x + s)%nat) (n - s).
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac