diff --git a/thue-morse.v b/thue-morse.v
index bbb23c2..782cd05 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -681,6 +681,8 @@ A010060  Thue-Morse sequence: let A_k denote the first 2^k terms; then A_0 = 0 a
                                    *)  
 
 Require Import Coq.Lists.List.
+Require Import PeanoNat.
+Require Import Nat.
 Require Import Nat.
 Require Import Bool.
 
@@ -804,8 +806,8 @@ Proof.
   - simpl tm_step. rewrite tm_morphism_rev.
     replace (tm_morphism (tm_step n)) with (tm_step (S n)).
     rewrite IHn. simpl tm_morphism. simpl tl.
-    rewrite PeanoNat.Nat.even_succ.
-    rewrite PeanoNat.Nat.odd_succ.
+    rewrite Nat.even_succ.
+    rewrite Nat.odd_succ.
     rewrite negb_involutive.
     reflexivity. reflexivity.
 Qed.
@@ -825,7 +827,7 @@ Proof.
   destruct n.
   - reflexivity.
   - rewrite tm_step_end_2. simpl.
-    rewrite PeanoNat.Nat.odd_succ.
+    rewrite Nat.odd_succ.
     reflexivity.
 Qed.
 
@@ -867,13 +869,18 @@ Proof.
       rewrite H1. easy.
       rewrite nth_error_Some in I. rewrite tm_size_power2 in I.
       assert (2^k <= length l1 + 2^k).
-      apply PeanoNat.Nat.le_add_l.
+      apply Nat.le_add_l.
       generalize I. generalize H3.
-      apply PeanoNat.Nat.le_lt_trans.
+      apply Nat.le_lt_trans.
     }
 
   assert (k < n). {
-    generalize H3. apply PeanoNat.Nat.pow_lt_mono_r_iff. 
+    generalize H3. apply Nat.pow_lt_mono_r_iff. 
+
+    BEFORE REPLACEMENT.
+
+
+