proposition: Lemma uniqueness_step2 : forall f x l, derivable_pt_lim f x l -> limit1_in (fun h => (f (x + h) - f x) / h) (fun h : C => h <> C0) l C0.
proof: Proof. unfold derivable_pt_lim, limit1_in, limit_in. intros f x l Hf_deriv eps eps_pos ; destruct (Hf_deriv eps eps_pos) as ([alpha alpha_pos], Halpha) ; clear Hf_deriv ; exists alpha ; split ; [assumption |] ; intros h [h_neq Hh] ; simpl in * ; unfold C_dist in Hh ; rewrite Cminus_0_r in Hh. unfold C_dist. apply Halpha ; intuition. Qed.
imports: MyRIneq Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity Ranalysis_derivability Ranalysis_usual Ranalysis_facts Ranalysis_MVT Canalysis_diff Cprop_base Cnorm Ctacfield Cmet Canalysis_def Cderiv