Remove dead code in ZUtil (shiftl_by)

1 files changed, 0 insertions, 20 deletions

diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 8e3d34ce4..54ab65115 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -796,26 +796,6 @@ Module Z.
   Hint Rewrite Z.shiftr_succ using zutil_arith : push_Zshift.
   Hint Rewrite <- Z.shiftr_succ using zutil_arith : pull_Zshift.
 
-  Definition shiftl_by n a := Z.shiftl a n.
-
-  Lemma shiftl_by_mul_pow2 : forall n a, 0 <= n -> Z.mul (2 ^ n) a = Z.shiftl_by n a.
-  Proof.
-    intros.
-    unfold Z.shiftl_by.
-    rewrite Z.shiftl_mul_pow2 by assumption.
-    apply Z.mul_comm.
-  Qed.
-
-  Lemma map_shiftl : forall n l, 0 <= n -> map (Z.mul (2 ^ n)) l = map (Z.shiftl_by n) l.
-  Proof.
-    intros; induction l; auto using Z.shiftl_by_mul_pow2.
-    simpl.
-    rewrite IHl.
-    f_equal.
-    apply Z.shiftl_by_mul_pow2.
-    assumption.
-  Qed.
-
   Lemma pow2_lt_or_divides : forall a b, 0 <= b ->
     2 ^ a < 2 ^ b \/ (2 ^ a) mod 2 ^ b = 0.
   Proof.