proposition: Lemma Derive_const : forall (a x : R), Derive (fun _ => a) x = 0.
proof: Proof. intros a x. apply is_derive_unique. apply: is_derive_const. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv