proposition: Lemma diff_derivable f a v : differentiable f a -> derivable f a v.
proof: Proof. move=> dfa; apply/derivable1P/derivable1_diffP. by apply: differentiable_comp; rewrite ?scale0r ?add0r. 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