202604221529

Theorems for sum of constant function

Add SumFunctionOnSetConst and SumFunctionConst stating that summing a
constant function over a finite set equals the constant times the
cardinality of the set, together with corresponding proofs and an
example in the doc comments.

[Feature]

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>