proposition: Lemma derivable_pt_lim_in_id : forall D x, derivable_pt_lim_in D id x 1.
proof: Proof. intros ; apply derivable_pt_lim_derivable_pt_lim_in, derivable_pt_lim_id. 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