proposition: Lemma deriveD f g (x v : V) : derivable f x v -> derivable g x v -> 'D_v (f + g) x = 'D_v f x + 'D_v g x.
proof: Proof. by move=> df dg; apply: cvg_lim (der_add df dg). 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