diff --git a/thue-morse.v b/thue-morse.v
index a54b476..f190a16 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -1416,30 +1416,6 @@ Require Import BinPos.
 
 
 
-(*
-PeanoNat.Nat.log2_spec_alt:
-  forall a : nat,
-  0 < a ->
-  exists r : nat,
-    a = 2 ^ PeanoNat.Nat.log2 a + r /\ 0 <= r < 2 ^ PeanoNat.Nat.log2 a
-N.log2_spec_alt:
-  forall a : N,
-  (0 < a)%N ->
-  exists r : N, a = (2 ^ N.log2 a + r)%N /\ (0 <= r < 2 ^ N.log2 a)%N
-
-
-PeanoNat.Nat.log2_shiftl:
-  forall a n : nat,
-  a <> 0 ->
-  PeanoNat.Nat.log2 (PeanoNat.Nat.shiftl a n) = PeanoNat.Nat.log2 a + n
-
-
-
- *)
-
-
-
-
 (* Hamming weight of a positive; argument can not be 0! *)
 Fixpoint hamming_weight_positive (x: positive) :=
   match x with