proposition: Fact dcomp (U V' W' : normedModType R) (f : U -> V') (g : V' -> W') x : differentiable f x -> differentiable g (f x) -> continuous ('d g (f x) \o 'd f x) /\ forall y, g (f (y + x)) = g (f x) + ('d g (f x) \o 'd f x) y +o_(y \near 0 : U) y.
proof: Proof. move=> df dg; split; first by move=> ?; apply: continuous_comp. apply: eqaddoEx => y; rewrite diff_locallyx// -addrA diff_locallyxC// linearD. rewrite addrA -addrA; congr (_ + _ + _). rewrite diff_eqO // ['d f x : _ -> _]diff_eqO //. by rewrite {2}eqoO addOx compOo_eqox compoO_eqox addox. 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