Skip to content

GitLab

Attention une mise à jour du serveur va être effectuée le vendredi 16 avril entre 12h et 12h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit 25b8177c authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files
Options

bitvectors: removed more Coq proofs

parent 63d61d3b
Hide whitespace changes
Inline Side-by-side
Showing with 122 additions and 649 deletions
examples/bitvectors/double_of_int/why3session.xml
View file @ 25b8177c
......@@ -104,7 +104,7 @@
</goal>
<goal name="mantissa_const_to_nat51" proved="true">
<proof prover="1"><result status="valid" time="0.18" steps="132"/></proof>
<proof prover="4"><result status="valid" time="0.93"/></proof>
<proof prover="4"><result status="valid" time="1.13"/></proof>
<proof prover="6" timelimit="11"><result status="valid" time="3.71"/></proof>
<proof prover="8"><result status="valid" time="0.75"/></proof>
</goal>
......@@ -148,7 +148,7 @@
<proof prover="4"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="nth_var31" proved="true">
<proof prover="1" timelimit="125"><result status="valid" time="4.10" steps="253"/></proof>
<proof prover="1" timelimit="125"><result status="valid" time="3.53" steps="253"/></proof>
<proof prover="4"><result status="valid" time="2.96"/></proof>
</goal>
<goal name="to_nat_sub_0_30" proved="true">
......@@ -169,7 +169,7 @@
<goal name="lemma1_pos" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="lemma1_pos.0" proved="true">
<proof prover="10" timelimit="10"><result status="valid" time="7.14" steps="1022"/></proof>
<proof prover="10" timelimit="10"><result status="valid" time="6.18" steps="1022"/></proof>
</goal>
</transf>
</goal>
......@@ -180,12 +180,12 @@
<proof prover="8"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="from_int2c_to_nat_sub_neg" proved="true">
<proof prover="5" timelimit="5" edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_neg_1.v"><result status="valid" time="2.50"/></proof>
<proof prover="5" timelimit="5" edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_neg_1.v"><result status="valid" time="1.93"/></proof>
</goal>
<goal name="lemma1_neg" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="lemma1_neg.0" proved="true">
<proof prover="10" timelimit="10"><result status="valid" time="5.21" steps="827"/></proof>
<proof prover="10" timelimit="10"><result status="valid" time="4.16" steps="827"/></proof>
</goal>
</transf>
</goal>
......@@ -197,7 +197,7 @@
<proof prover="8"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="nth_var_0_31" proved="true">
<proof prover="4" timelimit="10"><result status="valid" time="3.24"/></proof>
<proof prover="4" timelimit="10"><result status="valid" time="2.79"/></proof>
</goal>
<goal name="to_nat_bv32_bv64_aux" proved="true">
<transf name="introduce_premises" proved="true" >
......@@ -240,7 +240,7 @@
<goal name="lemma2.0.0" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="lemma2.0.0.0" proved="true">
<proof prover="11"><result status="valid" time="6.26"/></proof>
<proof prover="11"><result status="valid" time="3.80"/></proof>
</goal>
</transf>
</goal>
......@@ -259,7 +259,7 @@
<proof prover="8"><result status="valid" time="0.85"/></proof>
</goal>
<goal name="nth_var6" proved="true">
<proof prover="1"><result status="valid" time="1.41" steps="148"/></proof>
<proof prover="1"><result status="valid" time="1.17" steps="148"/></proof>
<proof prover="4"><result status="valid" time="1.74"/></proof>
<proof prover="8"><result status="valid" time="0.83"/></proof>
</goal>
......@@ -300,7 +300,7 @@
<proof prover="8"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="var_value0" proved="true">
<proof prover="5" timelimit="0" memlimit="0" edited="double_of_int_DoubleOfInt_var_value0_1.v"><result status="valid" time="4.20"/></proof>
<proof prover="5" timelimit="0" memlimit="0" edited="double_of_int_DoubleOfInt_var_value0_1.v"><result status="valid" time="3.39"/></proof>
</goal>
<goal name="from_int_sum" proved="true">
<proof prover="1"><result status="valid" time="0.05" steps="92"/></proof>
......
examples/bitvectors/power2.why
View file @ 25b8177c
......@@ -139,7 +139,7 @@ theory Pow2real
lemma Power_neg : forall n:int. pow2 (-n) = 1.0 /. pow2 n
lemma Power_sum_aux : forall n m: int. m >= 0 -> pow2 (n+m) = pow2 n *. pow2 m
lemma Power_sum_aux : forall m n. m >= 0 -> pow2 (n+m) = pow2 n *. pow2 m
lemma Power_sum : forall n m: int. pow2 (n+m) = pow2 n *. pow2 m
......
examples/bitvectors/power2/power2_Pow2int_Mod_pow2_gen_1.v deleted 100644 → 0
View file @ 63d61d3b
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
Parameter pow2: Z -> Z.
Axiom Power_0 : ((pow2 0%Z) = 1%Z).
Axiom Power_s :
forall (n:Z), (0%Z <= n)%Z -> ((pow2 (n + 1%Z)%Z) = (2%Z * (pow2 n))%Z).
Axiom Power_1 : ((pow2 1%Z) = 2%Z).
Axiom Power_sum :
forall (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) ->
((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%Z).
Axiom pow2pos : forall (i:Z), (0%Z <= i)%Z -> (0%Z < (pow2 i))%Z.
Axiom pow2_0 : ((pow2 0%Z) = 1%Z).
Axiom pow2_1 : ((pow2 1%Z) = 2%Z).
Axiom pow2_2 : ((pow2 2%Z) = 4%Z).
Axiom pow2_3 : ((pow2 3%Z) = 8%Z).
Axiom pow2_4 : ((pow2 4%Z) = 16%Z).
Axiom pow2_5 : ((pow2 5%Z) = 32%Z).
Axiom pow2_6 : ((pow2 6%Z) = 64%Z).
Axiom pow2_7 : ((pow2 7%Z) = 128%Z).
Axiom pow2_8 : ((pow2 8%Z) = 256%Z).
Axiom pow2_9 : ((pow2 9%Z) = 512%Z).
Axiom pow2_10 : ((pow2 10%Z) = 1024%Z).
Axiom pow2_11 : ((pow2 11%Z) = 2048%Z).
Axiom pow2_12 : ((pow2 12%Z) = 4096%Z).
Axiom pow2_13 : ((pow2 13%Z) = 8192%Z).
Axiom pow2_14 : ((pow2 14%Z) = 16384%Z).
Axiom pow2_15 : ((pow2 15%Z) = 32768%Z).
Axiom pow2_16 : ((pow2 16%Z) = 65536%Z).
Axiom pow2_17 : ((pow2 17%Z) = 131072%Z).
Axiom pow2_18 : ((pow2 18%Z) = 262144%Z).
Axiom pow2_19 : ((pow2 19%Z) = 524288%Z).
Axiom pow2_20 : ((pow2 20%Z) = 1048576%Z).
Axiom pow2_21 : ((pow2 21%Z) = 2097152%Z).
Axiom pow2_22 : ((pow2 22%Z) = 4194304%Z).
Axiom pow2_23 : ((pow2 23%Z) = 8388608%Z).
Axiom pow2_24 : ((pow2 24%Z) = 16777216%Z).
Axiom pow2_25 : ((pow2 25%Z) = 33554432%Z).
Axiom pow2_26 : ((pow2 26%Z) = 67108864%Z).
Axiom pow2_27 : ((pow2 27%Z) = 134217728%Z).
Axiom pow2_28 : ((pow2 28%Z) = 268435456%Z).
Axiom pow2_29 : ((pow2 29%Z) = 536870912%Z).
Axiom pow2_30 : ((pow2 30%Z) = 1073741824%Z).
Axiom pow2_31 : ((pow2 31%Z) = 2147483648%Z).
Axiom pow2_32 : ((pow2 32%Z) = 4294967296%Z).
Axiom pow2_33 : ((pow2 33%Z) = 8589934592%Z).
Axiom pow2_34 : ((pow2 34%Z) = 17179869184%Z).
Axiom pow2_35 : ((pow2 35%Z) = 34359738368%Z).
Axiom pow2_36 : ((pow2 36%Z) = 68719476736%Z).
Axiom pow2_37 : ((pow2 37%Z) = 137438953472%Z).
Axiom pow2_38 : ((pow2 38%Z) = 274877906944%Z).
Axiom pow2_39 : ((pow2 39%Z) = 549755813888%Z).
Axiom pow2_40 : ((pow2 40%Z) = 1099511627776%Z).
Axiom pow2_41 : ((pow2 41%Z) = 2199023255552%Z).
Axiom pow2_42 : ((pow2 42%Z) = 4398046511104%Z).
Axiom pow2_43 : ((pow2 43%Z) = 8796093022208%Z).
Axiom pow2_44 : ((pow2 44%Z) = 17592186044416%Z).
Axiom pow2_45 : ((pow2 45%Z) = 35184372088832%Z).
Axiom pow2_46 : ((pow2 46%Z) = 70368744177664%Z).
Axiom pow2_47 : ((pow2 47%Z) = 140737488355328%Z).
Axiom pow2_48 : ((pow2 48%Z) = 281474976710656%Z).
Axiom pow2_49 : ((pow2 49%Z) = 562949953421312%Z).
Axiom pow2_50 : ((pow2 50%Z) = 1125899906842624%Z).
Axiom pow2_51 : ((pow2 51%Z) = 2251799813685248%Z).
Axiom pow2_52 : ((pow2 52%Z) = 4503599627370496%Z).
Axiom pow2_53 : ((pow2 53%Z) = 9007199254740992%Z).
Axiom pow2_54 : ((pow2 54%Z) = 18014398509481984%Z).
Axiom pow2_55 : ((pow2 55%Z) = 36028797018963968%Z).
Axiom pow2_56 : ((pow2 56%Z) = 72057594037927936%Z).
Axiom pow2_57 : ((pow2 57%Z) = 144115188075855872%Z).
Axiom pow2_58 : ((pow2 58%Z) = 288230376151711744%Z).
Axiom pow2_59 : ((pow2 59%Z) = 576460752303423488%Z).
Axiom pow2_60 : ((pow2 60%Z) = 1152921504606846976%Z).
Axiom pow2_61 : ((pow2 61%Z) = 2305843009213693952%Z).
Axiom pow2_62 : ((pow2 62%Z) = 4611686018427387904%Z).
Axiom pow2_63 : ((pow2 63%Z) = 9223372036854775808%Z).
Axiom Div_mult_inst :
forall (x:Z) (z:Z), (0%Z < x)%Z ->
((int.EuclideanDivision.div ((x * 1%Z)%Z + z)%Z x) =
(1%Z + (int.EuclideanDivision.div z x))%Z).
Axiom Div_double :
forall (x:Z) (y:Z), ((0%Z < y)%Z /\ ((y <= x)%Z /\ (x < (2%Z * y)%Z)%Z)) ->
((int.EuclideanDivision.div x y) = 1%Z).
Axiom Div_pow :
forall (x:Z) (i:Z), (0%Z < i)%Z ->
(((pow2 (i - 1%Z)%Z) <= x)%Z /\ (x < (pow2 i))%Z) ->
((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = 1%Z).
Axiom Div_double_neg :
forall (x:Z) (y:Z),
((((-2%Z)%Z * y)%Z <= x)%Z /\ ((x < (-y)%Z)%Z /\ ((-y)%Z < 0%Z)%Z)) ->
((int.EuclideanDivision.div x y) = (-2%Z)%Z).
Axiom Div_pow2 :
forall (x:Z) (i:Z), (0%Z < i)%Z ->
(((-(pow2 i))%Z <= x)%Z /\ (x < (-(pow2 (i - 1%Z)%Z))%Z)%Z) ->
((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = (-2%Z)%Z).
Open Scope Z_scope.
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 3; admit.
(* Why3 goal *)
Theorem Mod_pow2_gen :
forall (x:Z) (i:Z) (k:Z), ((0%Z <= k)%Z /\ (k < i)%Z) ->
((int.EuclideanDivision.mod1
(int.EuclideanDivision.div (x + (pow2 i))%Z (pow2 k)) 2%Z)
= (int.EuclideanDivision.mod1 (int.EuclideanDivision.div x (pow2 k)) 2%Z)).
(* Why3 intros x i k (h1,h2). *)
(* intros x i k (h1,h2). *)
intros x i k (h1,h2).
replace (x + pow2 i) with (pow2 k*pow2(i-k)+x).
2:ae.
rewrite int.EuclideanDivision.Div_mult.
2:ae.
replace (pow2 (i-k)) with (2*pow2(i-k-1)).
2:ae.
ae.
Admitted.
examples/bitvectors/power2/power2_Pow2int_Power_sum_1.v deleted 100644 → 0
View file @ 63d61d3b
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Parameter pow2: Z -> Z.
Axiom Power_0 : ((pow2 0%Z) = 1%Z).
Axiom Power_s :
forall (n:Z), (0%Z <= n)%Z -> ((pow2 (n + 1%Z)%Z) = (2%Z * (pow2 n))%Z).
Axiom Power_1 : ((pow2 1%Z) = 2%Z).
Open Scope Z_scope.
Require Import Why3.
(* Why3 goal *)
Theorem Power_sum :
forall (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) ->
((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%Z).
(* Why3 intros n m (h1,h2). *)
intros n m (Hn & Hm).
generalize Hm.
pattern m; apply Z_lt_induction; auto.
clear m Hm.
intros m Hind Hm.
assert (h:(m = 0 \/ m > 0)) by omega; destruct h.
why3 "alt-ergo"; admit.
replace m with ((m-1)+1) by omega.
rewrite Power_s; auto with zarith.
why3 "alt-ergo"; admit.
Admitted.
examples/bitvectors/power2/power2_Pow2int_pow2pos_1.v deleted 100644 → 0
View file @ 63d61d3b
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Parameter pow2: Z -> Z.
Axiom Power_0 : ((pow2 0%Z) = 1%Z).
Axiom Power_s : forall (n:Z), (0%Z <= n)%Z ->
((pow2 (n + 1%Z)%Z) = (2%Z * (pow2 n))%Z).
Axiom Power_1 : ((pow2 1%Z) = 2%Z).
Axiom Power_sum : forall (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) ->
((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%Z).
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 2; admit.
Open Scope Z_scope.
(* Why3 goal *)
Theorem pow2pos : forall (i:Z), (0%Z <= i)%Z -> (0%Z < (pow2 i))%Z.
(* Why3 intros i h1. *)
intros i Hi.
generalize Hi.
pattern i; apply Z_lt_induction; auto.
intros j Hind Hj.
assert (h: j=0 \/ j>0) by omega; destruct h.
ae.
replace j with ((j-1)+1) by omega.
ae.
Admitted.
examples/bitvectors/power2/power2_Pow2real_Pow2_int_real_1.v deleted 100644 → 0
View file @ 63d61d3b
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
Require real.Real.
Require real.RealInfix.
Require real.FromInt.
Parameter pow2: Z -> R.
Axiom Power_0 : ((pow2 0%Z) = 1%R).
Axiom Power_s :
forall (n:Z), (0%Z <= n)%Z -> ((pow2 (n + 1%Z)%Z) = (2%R * (pow2 n))%R).
Axiom Power_p :
forall (n:Z), (n <= 0%Z)%Z ->
((pow2 (n - 1%Z)%Z) = ((05 / 10)%R * (pow2 n))%R).
Axiom Power_s_all : forall (n:Z), ((pow2 (n + 1%Z)%Z) = (2%R * (pow2 n))%R).
Axiom Power_p_all :
forall (n:Z), ((pow2 (n - 1%Z)%Z) = ((05 / 10)%R * (pow2 n))%R).
Axiom Power_1_2 : ((05 / 10)%R = (1%R / 2%R)%R).
Axiom Power_1 : ((pow2 1%Z) = 2%R).
Axiom Power_neg1 : ((pow2 (-1%Z)%Z) = (05 / 10)%R).
Axiom Power_non_null_aux : forall (n:Z), (0%Z <= n)%Z -> ~ ((pow2 n) = 0%R).
Axiom Power_neg_aux :
forall (n:Z), (0%Z <= n)%Z -> ((pow2 (-n)%Z) = (1%R / (pow2 n))%R).
Axiom Power_non_null : forall (n:Z), ~ ((pow2 n) = 0%R).
Axiom Power_neg : forall (n:Z), ((pow2 (-n)%Z) = (1%R / (pow2 n))%R).
Axiom Power_sum_aux :
forall (n:Z) (m:Z), (0%Z <= m)%Z ->
((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%R).
Axiom Power_sum :
forall (n:Z) (m:Z), ((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%R).
Parameter pow21: Z -> Z.
Axiom Power_01 : ((pow21 0%Z) = 1%Z).
Axiom Power_s1 :
forall (n:Z), (0%Z <= n)%Z -> ((pow21 (n + 1%Z)%Z) = (2%Z * (pow21 n))%Z).
Axiom Power_11 : ((pow21 1%Z) = 2%Z).
Axiom Power_sum1 :
forall (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) ->
((pow21 (n + m)%Z) = ((pow21 n) * (pow21 m))%Z).
Axiom pow2pos : forall (i:Z), (0%Z <= i)%Z -> (0%Z < (pow21 i))%Z.
Axiom pow2_0 : ((pow21 0%Z) = 1%Z).
Axiom pow2_1 : ((pow21 1%Z) = 2%Z).
Axiom pow2_2 : ((pow21 2%Z) = 4%Z).
Axiom pow2_3 : ((pow21 3%Z) = 8%Z).
Axiom pow2_4 : ((pow21 4%Z) = 16%Z).
Axiom pow2_5 : ((pow21 5%Z) = 32%Z).
Axiom pow2_6 : ((pow21 6%Z) = 64%Z).
Axiom pow2_7 : ((pow21 7%Z) = 128%Z).
Axiom pow2_8 : ((pow21 8%Z) = 256%Z).
Axiom pow2_9 : ((pow21 9%Z) = 512%Z).
Axiom pow2_10 : ((pow21 10%Z) = 1024%Z).
Axiom pow2_11 : ((pow21 11%Z) = 2048%Z).
Axiom pow2_12 : ((pow21 12%Z) = 4096%Z).
Axiom pow2_13 : ((pow21 13%Z) = 8192%Z).
Axiom pow2_14 : ((pow21 14%Z) = 16384%Z).
Axiom pow2_15 : ((pow21 15%Z) = 32768%Z).
Axiom pow2_16 : ((pow21 16%Z) = 65536%Z).
Axiom pow2_17 : ((pow21 17%Z) = 131072%Z).
Axiom pow2_18 : ((pow21 18%Z) = 262144%Z).
Axiom pow2_19 : ((pow21 19%Z) = 524288%Z).
Axiom pow2_20 : ((pow21 20%Z) = 1048576%Z).
Axiom pow2_21 : ((pow21 21%Z) = 2097152%Z).
Axiom pow2_22 : ((pow21 22%Z) = 4194304%Z).
Axiom pow2_23 : ((pow21 23%Z) = 8388608%Z).
Axiom pow2_24 : ((pow21 24%Z) = 16777216%Z).
Axiom pow2_25 : ((pow21 25%Z) = 33554432%Z).
Axiom pow2_26 : ((pow21 26%Z) = 67108864%Z).
Axiom pow2_27 : ((pow21 27%Z) = 134217728%Z).
Axiom pow2_28 : ((pow21 28%Z) = 268435456%Z).
Axiom pow2_29 : ((pow21 29%Z) = 536870912%Z).
Axiom pow2_30 : ((pow21 30%Z) = 1073741824%Z).
Axiom pow2_31 : ((pow21 31%Z) = 2147483648%Z).
Axiom pow2_32 : ((pow21 32%Z) = 4294967296%Z).
Axiom pow2_33 : ((pow21 33%Z) = 8589934592%Z).
Axiom pow2_34 : ((pow21 34%Z) = 17179869184%Z).
Axiom pow2_35 : ((pow21 35%Z) = 34359738368%Z).
Axiom pow2_36 : ((pow21 36%Z) = 68719476736%Z).
Axiom pow2_37 : ((pow21 37%Z) = 137438953472%Z).
Axiom pow2_38 : ((pow21 38%Z) = 274877906944%Z).
Axiom pow2_39 : ((pow21 39%Z) = 549755813888%Z).
Axiom pow2_40 : ((pow21 40%Z) = 1099511627776%Z).
Axiom pow2_41 : ((pow21 41%Z) = 2199023255552%Z).
Axiom pow2_42 : ((pow21 42%Z) = 4398046511104%Z).
Axiom pow2_43 : ((pow21 43%Z) = 8796093022208%Z).
Axiom pow2_44 : ((pow21 44%Z) = 17592186044416%Z).
Axiom pow2_45 : ((pow21 45%Z) = 35184372088832%Z).
Axiom pow2_46 : ((pow21 46%Z) = 70368744177664%Z).
Axiom pow2_47 : ((pow21 47%Z) = 140737488355328%Z).
Axiom pow2_48 : ((pow21 48%Z) = 281474976710656%Z).
Axiom pow2_49 : ((pow21 49%Z) = 562949953421312%Z).
Axiom pow2_50 : ((pow21 50%Z) = 1125899906842624%Z).
Axiom pow2_51 : ((pow21 51%Z) = 2251799813685248%Z).
Axiom pow2_52 : ((pow21 52%Z) = 4503599627370496%Z).
Axiom pow2_53 : ((pow21 53%Z) = 9007199254740992%Z).
Axiom pow2_54 : ((pow21 54%Z) = 18014398509481984%Z).
Axiom pow2_55 : ((pow21 55%Z) = 36028797018963968%Z).
Axiom pow2_56 : ((pow21 56%Z) = 72057594037927936%Z).
Axiom pow2_57 : ((pow21 57%Z) = 144115188075855872%Z).
Axiom pow2_58 : ((pow21 58%Z) = 288230376151711744%Z).
Axiom pow2_59 : ((pow21 59%Z) = 576460752303423488%Z).
Axiom pow2_60 : ((pow21 60%Z) = 1152921504606846976%Z).
Axiom pow2_61 : ((pow21 61%Z) = 2305843009213693952%Z).
Axiom pow2_62 : ((pow21 62%Z) = 4611686018427387904%Z).
Axiom pow2_63 : ((pow21 63%Z) = 9223372036854775808%Z).
Axiom Div_mult_inst :
forall (x:Z) (z:Z), (0%Z < x)%Z ->
((int.EuclideanDivision.div ((x * 1%Z)%Z + z)%Z x) =
(1%Z + (int.EuclideanDivision.div z x))%Z).
Axiom Div_double :
forall (x:Z) (y:Z), ((0%Z < y)%Z /\ ((y <= x)%Z /\ (x < (2%Z * y)%Z)%Z)) ->
((int.EuclideanDivision.div x y) = 1%Z).
Axiom Div_pow :