proposition: Lemma is_derive_unique f x l : is_derive f x l -> Derive f x = l.
proof: Proof. intros H. apply (@f_equal _ _ real _ l). apply is_lim_unique. apply is_lim_spec. apply is_derive_Reals in H. intros eps. destruct (H eps (cond_pos _)) as [d Hd]. exists d => h. rewrite /ball /= /AbsRing_ball /= /minus /plus /opp /= Ropp_0 Rplus_0_r. intros Hu Zu. now apply Hd. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv