proposition: Lemma differentiable_pt_lim_id : forall x v, differentiable_pt_lim id x v C1.
proof: Proof. intros x v v_neq ; unfold differentiable_pt_lim in |- *. intros eps Heps; exists (mkposreal eps Heps); intros h H1 H2; unfold id in |- *; replace ((x + h * v - x) / (h * v) - C1) with C0. rewrite Cnorm_C0 ; assumption. replace (x + h * v - x) with (h * v) by ring. replace (h *v / (h *v)) with C1. unfold Cminus ; rewrite Cadd_opp_r ; reflexivity. unfold Cdiv ; rewrite Cinv_r ; trivial. apply Cmult_integral_contrapositive_currified ; [apply IRC_neq_0_compat |] ; assumption. Qed.
imports: Cprop_base Cnorm Ctacfield Canalysis_def