proposition: Lemma is_C_derive_unique (f : C -> C) (z l : C) : is_derive f z l -> C_derive f z = l.
proof: Proof. intros [_ Df]. specialize (Df _ (fun P H => H)). apply is_C_lim_unique. intros P HP. destruct HP as [eps HP]. destruct (Df (pos_div_2 eps)) as [eps' Df']. unfold filtermap, locally', within. apply locally_C. exists eps'. intros y Hy Hyz. apply HP. assert (y - z <> 0). contradict Hyz. replace y with (y - z + z) by ring. rewrite Hyz. apply Cplus_0_l. apply: norm_compat1. rewrite /minus /plus /opp /=. replace ((f y - f z) / (y - z) + - l) with ((f y + - f z + - ((y + - z) * l)) / (y + - z)). 2: by field. rewrite /norm /= Cmod_div => //. apply Rlt_div_l. by apply Cmod_gt_0. eapply Rle_lt_trans. apply (Df' y Hy). simpl. rewrite /Rdiv Rmult_assoc. apply Rmult_lt_compat_l. by apply eps. rewrite Rmult_comm Rlt_div_l. rewrite /norm /minus /plus /opp /= /abs /=. apply Rminus_lt_0 ; ring_simplify. by apply Cmod_gt_0. by apply Rlt_0_2. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy