proposition: Lemma differential_pt_eq_0 : forall f x v l (pr:differentiable_pt f x v), v <> 0 -> differentiable_pt_lim f x v l -> differential_pt f x v pr = l.
proof: Proof. intros f x v l pr v_neq ; destruct (differential_pt_eq f x v l pr) ; assumption. Qed.
imports: Cprop_base Cnorm Ctacfield Canalysis_def