proposition: Lemma is_derive_const : forall (a : V) (x : K), is_derive (fun _ : K => a) x zero.
proof: Proof. intros a x. apply filterdiff_ext_lin with (fun y : K => zero). apply filterdiff_const. intros y. apply sym_eq. apply: scal_zero_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv