proposition: Lemma diff_locally (x : V) (f : V -> W) : differentiable f x -> (f \o shift x = cst (f x) + 'd f x +o_ (0 : V) id).
proof: Proof. by move=> /diff_locallyP []. 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