proposition: Lemma Derive_n_const n a : forall x, Derive_n (fun _ => a) (S n) x = 0.
proof: Proof. intros x ; apply is_derive_n_unique, is_derive_n_const. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv