proposition: Lemma is_derive_n_ext_loc : forall f g n x l, locally x (fun t => f t = g t) -> is_derive_n f n x l -> is_derive_n g n x l.
proof: Proof. intros f g n x l Heq. case: n => /= [ | n]. move => <- ; apply sym_eq. pattern x ; now apply locally_singleton. apply is_derive_ext_loc. apply locally_locally in Heq. apply filter_imp with (2 := Heq) => {Heq}. by apply Derive_n_ext_loc. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv