proposition: Lemma differentiableV (f : V -> R) x : differentiable f x -> f x != 0 -> differentiable (fun y => (f y)^-1) x.
proof: Proof. by move=> df fxn0; apply: differentiable_comp _ (differentiable_Rinv fxn0). 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