proposition: Lemma ex_derive_n_const a n x: ex_derive_n (fun _ => a) n x.
proof: Proof. case: n => //= ; case => //= [ | n]. apply ex_derive_const. eapply ex_derive_ext. intros t ; apply sym_equal, is_derive_unique, is_derive_n_const. by apply ex_derive_const. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv