proposition: Lemma ex_derive_n_ext_loc : forall f g n x, locally x (fun t => f t = g t) -> ex_derive_n f n x -> ex_derive_n g n x.
proof: Proof. intros f g n x Heq. case: n => /= [ | n]. by []. apply ex_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