proposition: Lemma differential_pt_eq : forall f x v l (pr:differentiable_pt f x v), v <> 0 -> (differential_pt f x v pr = l <-> differentiable_pt_lim f x v l).
proof: Proof. intros f x v l pr v_neq ; split ; intro Hf_deriv. assert (H := proj2_sig pr) ; unfold derive_pt in Hf_deriv ; rewrite Hf_deriv in H ; assumption. assert (H := proj2_sig pr) ; unfold derivable_pt_abs in H. assert (H' := uniqueness_limite _ _ _ _ (proj1_sig pr) v_neq Hf_deriv H) ; symmetry ; assumption. Qed.
imports: Cprop_base Cnorm Ctacfield Canalysis_def