diff --git a/thue-morse.v b/thue-morse.v
index 542a822..039b975 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -58,10 +58,8 @@ Proof.
   - reflexivity.
   - simpl. rewrite negb_map_explode.
     rewrite IHl. rewrite tm_morphism_concat.
-    rewrite <- app_assoc.
-    replace (map negb [a]) with ([negb a]). simpl.
+    rewrite <- app_assoc. simpl.
     rewrite negb_involutive. reflexivity.
-    reflexivity.
 Qed.
 
 Lemma tm_morphism_double_index : forall (l : list bool) (k : nat),
@@ -393,9 +391,9 @@ Proof.
 
       apply H1. apply H2.
   - induction j.
-    + intros L. rewrite Nat.add_0_r in L. rewrite Nat.add_0_r in L.
+    + intro L. rewrite Nat.add_0_r in L. rewrite Nat.add_0_r in L.
       apply tm_step_next_range2_flip_two. apply H. apply I. apply L.
-    + intros L.
+    + intro L.
       rewrite Nat.add_succ_r in L. rewrite Nat.add_succ_r in L.
 
       assert (2^n < 2^(S n + j)).
@@ -611,33 +609,19 @@ Qed.
 
 
 
-(* vérifier si les deux sont nécessaires *)
-Require Import BinPosDef.
-Require Import BinPos.
-
-Theorem tm_step_double_index : forall (p : positive),
-  nth_error (tm_step (Pos.size_nat p)) (Pos.to_nat p)
-  = nth_error (tm_step (S (Pos.size_nat p))) (Pos.to_nat (xO p)).
-Proof.
-  intros p.
-  induction p.
-
-
-
-
-
-
 
 
 
 
   (* TODO: supprimer head_2 *)
 
+(* vérifier si les deux sont nécessaires *)
+Require Import BinPosDef.
+Require Import BinPos.
 
 Require Import BinNat.
 
 
-
 (* Hamming weight of a positive; argument can not be 0! *)
 Fixpoint hamming_weight_positive (x: positive) :=
   match x with