proposition: Lemma pr_nu_var2 : forall (f g:R -> R) (x:R) (pr1:derivable_pt f x) (pr2:derivable_pt g x), (forall h:R, f h = g h) -> derive_pt f x pr1 = derive_pt g x pr2.
proof: Proof. unfold derivable_pt, derive_pt; intros f g x (x0,p0) (x1,p1) H. assert (H0 := uniqueness_step2 _ _ _ p0). assert (H1 := uniqueness_step2 _ _ _ p1). cut (limit1_in (fun h:R => (f (x + h) - f x) / h) (fun h:R => h <> 0) x1 0). - intro H2; assert (H3 := uniqueness_step1 _ _ _ _ H0 H2). assumption. - unfold limit1_in; unfold limit_in; unfold dist; simpl; unfold Rdist; unfold limit1_in in H1; unfold limit_in in H1; unfold dist in H1; simpl in H1; unfold Rdist in H1. intros; elim (H1 eps H2); intros. elim H3; intros. exists x2. split. + assumption. + intros; do 2 rewrite H; apply H5; assumption. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Ranalysis3 Exp_prop MVT Lra Lia