From ec41af7ac01cef7c30785e6dd704381f31e7c2d3 Mon Sep 17 00:00:00 2001
From: ckeller <ckeller@users.noreply.github.com>
Date: Thu, 14 Feb 2019 20:09:40 +0100
Subject: V8.7 (#36)

Port SMTCoq to Coq-8.7
---
 src/versions/standard/Int63/Int63Axioms_standard.v | 31 +++++++++++++++++++++-
 1 file changed, 30 insertions(+), 1 deletion(-)

(limited to 'src/versions/standard/Int63/Int63Axioms_standard.v')

diff --git a/src/versions/standard/Int63/Int63Axioms_standard.v b/src/versions/standard/Int63/Int63Axioms_standard.v
index d4e45fc..9a90d39 100644
--- a/src/versions/standard/Int63/Int63Axioms_standard.v
+++ b/src/versions/standard/Int63/Int63Axioms_standard.v
@@ -11,12 +11,41 @@
 
 
 Require Import Bvector.
-Require Export BigNumPrelude.
+(* Require Export BigNumPrelude. *)
 Require Import Int31 Cyclic31.
 Require Export Int63Native.
 Require Export Int63Op.
 Require Import Psatz.
 
+Local Open Scope Z_scope.
+
+
+(* Taken from BigNumPrelude *)
+
+ Lemma div_le_0 : forall p x, 0 <= x -> 0 <= x / 2 ^ p.
+ Proof.
+  intros p x Hle;destruct (Z_le_gt_dec 0 p).
+  apply  Zdiv_le_lower_bound;auto with zarith.
+  replace (2^p) with 0.
+  destruct x;compute;intro;discriminate.
+  destruct p;trivial;discriminate.
+ Qed.
+
+ Lemma div_lt : forall p x y, 0 <= x < y -> x / 2^p < y.
+ Proof.
+  intros p x y H;destruct (Z_le_gt_dec 0 p).
+  apply Zdiv_lt_upper_bound;auto with zarith.
+  apply Z.lt_le_trans with y;auto with zarith.
+  rewrite <- (Z.mul_1_r y);apply Z.mul_le_mono_nonneg;auto with zarith.
+  assert (0 < 2^p);auto with zarith.
+  replace (2^p) with 0.
+  destruct x;change (0<y);auto with zarith.
+  destruct p;trivial;discriminate.
+ Qed.
+
+
+(* Int63Axioms *)
+
 Definition wB := (2^(Z_of_nat size)).
 
 Notation "[| x |]" := (to_Z x)  (at level 0, x at level 99) : int63_scope.
-- 
cgit