added a lemma in int.Sum

parent 99509932
......@@ -366,6 +366,11 @@ theory Sum
(forall i. a <= i <= b -> f i = g i) ->
sum a b f = sum a b g
lemma sum_le:
forall f g: int -> int, a b: int.
(forall i. a <= i <= b -> f i <= g i) ->
sum a b f <= sum a b g
lemma sum_nonneg:
forall f: int -> int, a b: int.
(forall i. a <= i <= b -> 0 <= f i) ->
......
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