proposition: Lemma diffV (f : V -> R) x : differentiable f x -> f x != 0 -> 'd (fun y => (f y)^-1) x = - (f x) ^- 2 \*: 'd f x :> (V -> R).
proof: Proof. move=> df fxn0. by rewrite [LHS](diff_comp df (differentiable_Rinv fxn0)) diff_Rinv. 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