Deletion of useless Zdigits_def

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

1 files changed, 2 insertions, 24 deletions

diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 379e68544..9e559b68c 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -992,12 +992,7 @@ Proof.
   rewrite ?Pos.pred_N_succ; now destruct n.
 Qed.
 
-Lemma div2_of_N n : of_N (N.div2 n) = div2 (of_N n).
-Proof.
- now destruct n as [|[ | | ]].
-Qed.
-
-(** Correctness proofs about [Zshiftr] and [Zshiftl] *)
+(** Correctness proofs about [Z.shiftr] and [Z.shiftl] *)
 
 Lemma shiftr_spec_aux a n m : 0<=n -> 0<=m ->
  testbit (shiftr a n) m = testbit a (m+n).
@@ -1016,7 +1011,7 @@ Proof.
  now rewrite 2 testbit_0_l.
  (* a > 0 *)
  change (Zpos a) with (of_N (Npos a)) at 1.
- rewrite <- (Pos.iter_swap_gen _ _ _ Ndiv2) by exact div2_of_N.
+ rewrite <- (Pos.iter_swap_gen _ _ _ Ndiv2) by now intros [|[ | | ]].
  rewrite testbit_Zpos, testbit_of_N', H; trivial.
  exact (N.shiftr_spec' (Npos a) (Npos n) (to_N m)).
  (* a < 0 *)
@@ -1155,23 +1150,6 @@ Proof.
  now rewrite N.lxor_spec, xorb_negb_negb.
 Qed.
 
-(** An additionnal proof concerning [Pos.shiftl_nat], used in BigN *)
-
-Lemma pos_shiftl_nat_pow n p :
-  Zpos (Pos.shiftl_nat p n) = Zpos p * 2 ^ Z.of_nat n.
-Proof.
- intros.
- rewrite mul_comm.
- induction n. simpl; auto.
- transitivity (2 * (2 ^ Z.of_nat n * Zpos p)).
- rewrite <- IHn. auto.
- rewrite mul_assoc.
- replace (of_nat (S n)) with (succ (of_nat n)).
- rewrite <- pow_succ_r. trivial.
- now destruct n.
- destruct n. trivial. simpl. now rewrite Pos.add_1_r.
-Qed.
-
 (** ** Induction principles based on successor / predecessor *)
 
 Lemma peano_ind (P : Z -> Prop) :