proposition: Lemma extension_C1_ex_derive (f df : R -> R) (a b : Rbar) : Rbar_le a b -> (forall x : R, Rbar_le a x -> Rbar_le x b -> ex_derive f x) -> forall x : R, ex_derive (extension_C1 f (Derive f) a b) x.
proof: Proof. intros Hab Df x. eexists. apply extension_C1_is_derive => //. intros y Hay Hby. by apply Derive_correct, Df. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv