proposition: Lemma Derive_ext : forall f g x, (forall t, f t = g t) -> Derive f x = Derive g x.
proof: Proof. intros f g x Hfg. apply Derive_ext_loc. by apply filter_forall. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv