proposition: Lemma trigger_derive (R : realType) (f : R -> R) x x1 y1 : is_derive x (1 : R) f x1 -> x1 = y1 -> is_derive x 1 f y1.
proof: Proof. by move=> Hi <-. 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