proposition: Lemma derivable_nbhsx (f : V -> W) a v : derivable f a v -> forall h, f (a + h *: v) = f a + h *: 'D_v f a +o_(h \near (nbhs (0 : R))) h.
proof: Proof. move=> /derivable_nbhs; rewrite funeqE => df. by apply: eqaddoEx => h; have /= := (df h); rewrite addrC => ->. 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