proposition: Lemma derivable_pt_lim_id : forall x:R, derivable_pt_lim id x 1.
proof: Proof. intro; unfold derivable_pt_lim. intros eps Heps; exists (mkposreal eps Heps); intros h H1 H2; unfold id; replace ((x + h - x) / h - 1) with 0. - rewrite Rabs_R0; apply Rle_lt_trans with (Rabs h). + apply Rabs_pos. + assumption. - unfold Rminus; rewrite Rplus_assoc; rewrite (Rplus_comm x); rewrite Rplus_assoc. rewrite Rplus_opp_l; rewrite Rplus_0_r; unfold Rdiv; rewrite Rinv_r. + symmetry ; apply Rplus_opp_r. + assumption. Qed.
imports: Rbase Rfunctions Rlimit Rderiv