proposition: Lemma diff_comp (U V' W' : normedModType R) (f : U -> V') (g : V' -> W') x : differentiable f x -> differentiable g (f x) -> 'd (g \o f) x = 'd g (f x) \o 'd f x :> (U -> W').
proof: Proof. by move=> df dg; apply/diff_unique; have [? /funext] := dcomp df dg. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum matrix interval) mathcomp(mathcomp_extra boolp classical_sets functions) reals signed topology prodnormedzmodule normedtype landau forms