proposition: Lemma is_derive_eq f (x v : V) (df f' : W) : is_derive x v f f' -> f' = df -> is_derive x v f df.
proof: Proof. by move=> ? <-. 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