proposition: Lemma pr_nu_var : forall (f g:R -> R) (x:R) (pr1:derivable_pt f x) (pr2:derivable_pt g x), f = g -> 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) ->. apply uniqueness_limite with g x; assumption. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Ranalysis3 Exp_prop MVT Lra Lia