proposition: Lemma derive1E V (f : R -> V) a : f^`() a = 'D_1 f a.
proof: Proof. rewrite /derive1 /derive; set d := (fun _ : R => _); set d' := (fun _ : R => _). by suff -> : d = d' by []; rewrite funeqE=> h; rewrite /d /d' /= [h%:A](mulr1). 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