proposition: Lemma uniqueness_step1 : forall f (x l1 l2:R), limit1_in (fun h:R => (f (x + h) - f x) / h) (fun h:R => h <> 0) l1 0 -> limit1_in (fun h:R => (f (x + h) - f x) / h) (fun h:R => h <> 0) l2 0 -> l1 = l2.
proof: Proof. intros; apply (single_limit (fun h:R => (f (x + h) - f x) / h) ( fun h:R => h <> 0) l1 l2 0); try assumption. unfold adhDa; intros; exists (alp / 2). split. - unfold Rdiv; apply prod_neq_R0. + red; intro; rewrite H2 in H1; elim (Rlt_irrefl _ H1). + apply Rinv_neq_0_compat; discrR. - unfold Rdist; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; unfold Rdiv; rewrite Rabs_mult. replace (Rabs (/ 2)) with (/ 2). + replace (Rabs alp) with alp. * apply Rmult_lt_reg_l with 2. -- prove_sup0. -- rewrite (Rmult_comm 2); rewrite Rmult_assoc; rewrite Rinv_l; [ idtac | discrR ]; rewrite Rmult_1_r; rewrite <-Rplus_diag; pattern alp at 1; replace alp with (alp + 0); [ idtac | ring ]; apply Rplus_lt_compat_l; assumption. * symmetry ; apply Rabs_right; left; assumption. + symmetry ; apply Rabs_right; left; change (0 < / 2); apply Rinv_0_lt_compat; prove_sup0. Qed.
imports: Rbase Rfunctions Rlimit Rderiv