Commit 2d539148 authored by MARCHE Claude's avatar MARCHE Claude

theory int.Power : one more lemma

parent b92d65ff
......@@ -79,6 +79,13 @@ rewrite 3!power_is_exponentiation ; auto with zarith.
apply Power_mult2 ; auto with zarith.
Qed.
(* Why3 goal *)
Lemma Power_non_neg : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z <= y)%Z) ->
(0%Z <= (power x y))%Z.
intros x y (h1,h2).
now apply Z.pow_nonneg.
Qed.
Open Scope Z_scope.
(* Why3 goal *)
......
......@@ -235,6 +235,9 @@ theory Power
goal CommutativeMonoid.Unit_def_l, goal CommutativeMonoid.Unit_def_r,
goal CommutativeMonoid.Comm.Comm
lemma Power_non_neg:
forall x y. x >= 0 /\ y >= 0 -> power x y >= 0
lemma Power_monotonic:
forall x n m:int. 0 < x /\ 0 <= n <= m -> power x n <= power x m
......
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