proposition: Lemma is_derive_n_unique f n x l : is_derive_n f n x l -> Derive_n f n x = l.
proof: Proof. case n. easy. simpl; intros n0 H. now apply is_derive_unique. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv