proposition: Theorem derivable_pt_lim_eq : forall f g, (forall x, f x = g x) -> forall x l, derivable_pt_lim f x l -> derivable_pt_lim g x l.
proof: Proof. intros f g H x l. unfold derivable_pt_lim. intros. destruct (H0 _ H1) as (delta, H2). exists delta. intros. do 2 rewrite <- H. apply H2 ; assumption. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux)