diff --git a/thue-morse.v b/thue-morse.v
index 7ac71d5..a79cd29 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -741,6 +741,23 @@ Proof.
     reflexivity.
 Qed.
 
+Lemma tm_morphism_double_index : forall (l : list bool) (k : nat),
+  nth_error l k = nth_error (tm_morphism l) (2*k).
+Proof.
+  intros l.
+  induction l.
+  - intro k.
+    simpl. replace (nth_error [] k) with (None : option bool).
+    rewrite Nat.add_0_r. replace (nth_error [] (k+k)) with (None : option bool).
+    reflexivity. symmetry. apply nth_error_None. simpl. apply Nat.le_0_l.
+    symmetry. apply nth_error_None. simpl. apply Nat.le_0_l.
+  - intro k. induction k.
+    + rewrite Nat.mul_0_r. reflexivity.
+    + simpl. rewrite Nat.add_0_r. rewrite Nat.add_succ_r. simpl.
+      replace (k+k) with (2*k). apply IHl. simpl. rewrite Nat.add_0_r.
+      reflexivity.
+Qed.
+
 Lemma tm_build_negb : forall (l : list bool),
   tm_morphism (map negb l) = map negb (tm_morphism l).
 Proof.
@@ -822,6 +839,16 @@ Proof.
     reflexivity.
 Qed.
 
+Theorem tm_step_double_index : forall (n k : nat),
+  nth_error (tm_step n) k = nth_error (tm_step (S n)) (2*k).
+Proof.
+  intros n k.
+  destruct k.
+  - rewrite Nat.mul_0_r. rewrite tm_step_head_1. simpl.
+    rewrite tm_step_head_1. reflexivity.
+  - rewrite <- tm_step_lemma.
+    rewrite tm_morphism_double_index. reflexivity.
+Qed.
 
 Lemma tm_step_single_bit_index : forall (n : nat),
   nth_error (tm_step (S n)) (2^n) = Some true.
@@ -1266,35 +1293,6 @@ Proof.
   generalize P. generalize I. apply Nat.lt_le_trans.
 Qed.
 
-Lemma tm_morphism_double_index : forall (l : list bool) (k : nat),
-  nth_error l k = nth_error (tm_morphism l) (2*k).
-Proof.
-  intros l.
-  induction l.
-  - intro k.
-    simpl. replace (nth_error [] k) with (None : option bool).
-    rewrite Nat.add_0_r. replace (nth_error [] (k+k)) with (None : option bool).
-    reflexivity. symmetry. apply nth_error_None. simpl. apply Nat.le_0_l.
-    symmetry. apply nth_error_None. simpl. apply Nat.le_0_l.
-  - intro k. induction k.
-    + rewrite Nat.mul_0_r. reflexivity.
-    + simpl. rewrite Nat.add_0_r. rewrite Nat.add_succ_r. simpl.
-      replace (k+k) with (2*k). apply IHl. simpl. rewrite Nat.add_0_r.
-      reflexivity.
-Qed.
-
-Theorem tm_step_double_index : forall (n k : nat),
-  nth_error (tm_step n) k = nth_error (tm_step (S n)) (2*k).
-Proof.
-  intros n k.
-  destruct k.
-  - rewrite Nat.mul_0_r. rewrite tm_step_head_1. simpl.
-    rewrite tm_step_head_1. reflexivity.
-  - replace (tm_step (S n)) with (tm_morphism (tm_step n)).
-    rewrite tm_morphism_double_index. reflexivity. reflexivity.
-Qed.
-
-
 
 
 (* vérifier si les deux sont nécessaires *)