proposition: Lemma is_derive_comp : forall (f : K -> V) (g : K -> K) (x : K) (df : V) (dg : K), is_derive f (g x) df -> is_derive g x dg -> is_derive (fun x => f (g x)) x (scal dg df).
proof: Proof. intros f g x df dg Df Dg. eapply filterdiff_ext_lin. apply filterdiff_comp' with (1 := Dg) (2 := Df). simpl => y. apply sym_eq, scal_assoc. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv