proposition: Lemma is_deriveV (f : R -> R) (x t v : R) : f x != 0 -> is_derive x v f t -> is_derive x v (fun y => (f y)^-1) (- (f x) ^- 2 *: t).
proof: Proof. move=> fxNZ Df. constructor; first by apply: derivableV => //; case: Df. by rewrite deriveV //; case: Df => _ ->. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum finmap) mathcomp(matrix interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) ereal reals signed topology prodnormedzmodule normedtype derive sequences real_interval HB(structures)