From 6afa8653207732d3cd0e9d5a2d77665369036bf0 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 10 Feb 2009 23:53:02 +0000
Subject: Cyclic31: proof of a forgotten admit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11906 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Numbers/Cyclic/Int31/Cyclic31.v | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index c6ad147409..3835c6cde7 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -1637,7 +1637,12 @@ Section Int31_Spec.
  apply Zplus_eq_compat.
  ring.
  assert ((2*[|y|]) mod wB = 2*[|y|] - wB).
-  admit.
+  clear - H. symmetry. apply Zmod_unique with 1; [ | ring ].
+  generalize (phi_lowerbound  _ H) (phi_bounded y).
+  set (wB' := 2^Z_of_nat (pred size)).
+  replace wB with (2*wB'); [ omega | ].
+  unfold wB'. rewrite <- Zpower_Zsucc, <- inj_S by (auto with zarith).
+  f_equal.
  rewrite H1.
  replace wB with (2^(Z_of_nat n)*2^(31-Z_of_nat n)) by  
   (rewrite <- Zpower_exp; auto with zarith; f_equal; unfold size; ring).
-- 
cgit v1.2.3