proposition: Lemma Derive_n_ext_loc : forall f g n x, locally x (fun t => f t = g t) -> Derive_n f n x = Derive_n g n x.
proof: Proof. intros f g n x Heq. pattern x ; apply locally_singleton. induction n. exact Heq. apply locally_locally in IHn. apply filter_imp with (2 := IHn) => {IHn}. intros t H. now apply Derive_ext_loc. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv