proposition: Lemma derivable_pt_lim_in_id: forall D x, derivable_pt_lim_in D id x 1.
proof: Proof. intros D x eps eps_pos ; exists eps ; intros ; split. assumption. intros y [[_ Hneq] _] ; unfold growth_rate, id ; simpl. apply Rle_lt_trans with (Rabs 0) ; [| rewrite Rabs_R0 ; assumption]. right ; apply Rabs_eq_compat ; field ; apply Rminus_eq_contra ; symmetry ; assumption. Qed.
imports: Rbase Ranalysis Rfunctions Rfunction_def MyRIneq Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_facts