proposition: Lemma derive_pt_id : forall x pr, derive_pt id x pr = 1.
proof: Proof. intros ; rewrite <- derive_pt_id with x ; apply pr_nu_var ; reflexivity. Qed.
imports: Rbase Rpower Ranalysis Lra Rfunctions Rfunction_def Rextensionality MyRIneq MyR_dist Rtopology Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity