proposition: Lemma C_Sn_derivable : forall f n, C (S n) f -> derivable f.
proof: Proof. intros. inversion H. subst. apply pr. Qed.
imports: Reals Rintegral Riemann_integrable Rfunction_classes Nth_derivative_def Lra Ring Ranalysis Rextensionality