proposition: Lemma is_derive_id : forall x : K, is_derive (fun t : K => t) x one.
proof: Proof. intros x. apply filterdiff_ext_lin with (fun t : K => t). apply filterdiff_id. rewrite /scal /=. intros y. apply sym_eq, mult_one_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv