proposition: Lemma is_derive_Sn (f : R -> R) (n : nat) (x l : R) : locally x (ex_derive f) -> (is_derive_n f (S n) x l <-> is_derive_n (Derive f) n x l).
proof: Proof. move => Hf. case: n => /= [ | n]. split => H. by apply is_derive_unique. rewrite -H ; apply Derive_correct. now apply locally_singleton. split => Hf'. - apply is_derive_ext with (2 := Hf'). move => y ; rewrite (Derive_n_comp _ n 1%nat). by (replace (n + 1)%nat with (S n) by ring). - apply is_derive_ext with (2 := Hf'). move => y ; rewrite (Derive_n_comp _ n 1%nat). by (replace (n + 1)%nat with (S n) by ring). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv