proposition: Lemma is_derive_n_const n a : forall x, is_derive_n (fun _ => a) (S n) x 0.
proof: Proof. elim: n => /= [ | n IH] x. by apply @is_derive_const. eapply is_derive_ext. intros t ; apply sym_equal, is_derive_unique, IH. by apply @is_derive_const. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv