fact: Fixpoint bernoullicoeff (n:nat) (k:nat) : R:= match n with | O => match k with | O => INR 1 | _ => INR 0 end |(S m)=> match k with | O => (sum_f_R0 (fun l => -((bernoullicoeff m l)*(/INR (S l))*(INR n)*/ INR (S (S l)) )) m) | (S l)=> (bernoullicoeff m l)*/(INR (S l))*(INR n) end end.
imports: Reals