proposition: Lemma differentiable_cst (W' : normedModType R) (a : W') (x : V) : differentiable (cst a) x.
proof: Proof. by apply/diff_locallyP; rewrite diff_cst; have := dcst a x. 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