proposition: Lemma diff_cst (V W : normedModType R) a x : ('d (cst a) x : V -> W) = 0.
proof: Proof. by apply/diff_unique; 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