theory int.Sum: new lemma sum_zero

parent 1ae06e11
......@@ -380,6 +380,11 @@ theory Sum
forall f: int -> int, a b c: int. a <= b <= c ->
sum a c f = sum a b f + sum b c f
lemma sum_zero:
forall f: int -> int, a b: int.
(forall i. a <= i < b -> f i = 0) ->
sum a b f = 0
end
(** {2 Factorial function} *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment