proposition: Lemma ex_derive_const : forall (a : V) (x : K), ex_derive (fun _ => a) x.
proof: Proof. intros a x. eexists. apply is_derive_const. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv