add_mul_pos uses int31 only

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9845 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 21 insertions, 1 deletions

diff --git a/theories/Ints/Z/ZDivModAux.v b/theories/Ints/Z/ZDivModAux.v
index d07b92d80e..be7955aadd 100644
--- a/theories/Ints/Z/ZDivModAux.v
+++ b/theories/Ints/Z/ZDivModAux.v
@@ -386,7 +386,7 @@ Hint Resolve Zlt_gt Zle_ge: zarith.
 
  Lemma shift_unshift_mod : forall n p a,
      0 <= a < 2^n ->
-     0 < p < n ->
+     0 <= p <= n ->
      a * 2^p = a / 2^(n - p) * 2^n + (a*2^p) mod 2^n.
  Proof.
   intros n p a H1 H2.
diff --git a/theories/Ints/Z/ZPowerAux.v b/theories/Ints/Z/ZPowerAux.v
index b56b52d49d..151b9a73ab 100644
--- a/theories/Ints/Z/ZPowerAux.v
+++ b/theories/Ints/Z/ZPowerAux.v
@@ -181,3 +181,23 @@ replace (a^c) with 0. auto with zarith.
 destruct c;trivial;unfold Zgt in z0;discriminate z0.
 destruct b;trivial;unfold Zgt in z;discriminate z.
 Qed.
+
+Theorem Zpower2_lt_lin: forall n,
+  0 <= n -> n < 2 ^ n.
+intros n; apply (natlike_ind (fun n => n < 2 ^n)); clear n.
+ simpl; auto with zarith.
+intros n H1 H2; unfold Zsucc.
+case (Zle_lt_or_eq _ _ H1); clear H1; intros H1.
+  apply Zle_lt_trans with (n + n); auto with zarith.
+  rewrite Zpower_exp; auto with zarith.
+  rewrite Zpower_exp_1.
+  assert (tmp: forall p, p * 2 = p + p); intros; try ring;
+  rewrite tmp; auto with zarith.
+subst n; simpl; unfold Zpower_pos; simpl; auto with zarith.
+Qed.
+
+Theorem Zpower2_le_lin: forall n,
+  0 <= n -> n <= 2 ^ n.
+intros; apply Zlt_le_weak.
+apply Zpower2_lt_lin; auto.
+Qed.