proposition: Lemma derive1_comp (R : realFieldType) (f g : R -> R) x : derivable f x 1 -> derivable g (f x) 1 -> (g \o f)^`() x = g^`() (f x) * f^`() x.
proof: Proof. move=> /derivable1_diffP df /derivable1_diffP dg. rewrite derive1E'; last exact/differentiable_comp. rewrite diff_comp // !derive1E' //= -[X in 'd _ _ X = _]mulr1. by rewrite [LHS]linearZ mulrC. 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