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