proposition: Lemma derivable_pt_in_id: forall (D : R -> Prop) (x : R), derivable_pt_in D id x.
proof: Proof. intros ; eexists ; eapply derivable_pt_lim_in_id. Qed.
imports: Rbase Ranalysis Rfunctions Rfunction_def MyRIneq Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_facts