proposition: Lemma C_Sm_derive_C_m : forall f n pr, C (S n) f -> C n (derive f pr).
proof: Proof. intros. inversion H. eapply C_ext. 2: apply H1. intro. apply pr_nu. Qed.
imports: Reals Rintegral Riemann_integrable Rfunction_classes Nth_derivative_def Lra Ring Ranalysis Rextensionality