proposition: Lemma is_diff_eq (V' W' : normedModType R) (f f' g : V' -> W') (x : V') : is_diff x f f' -> f' = g -> is_diff x f g.
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