diff --git a/thue-morse.v b/thue-morse.v
index 1cbdc53..30530b5 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -556,8 +556,7 @@ Proof.
   apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. apply Nat.lt_succ_diag_r.
   assumption.
 
-  assert (G: k = 0 \/ 0 < k). apply Nat.eq_0_gt_0_cases.
-  destruct G as [G1|G2].
+  assert (G: k = 0 \/ 0 < k). apply Nat.eq_0_gt_0_cases. destruct G as [G1|G2].
 
   (* k = 0 *)
   rewrite G1. rewrite Nat.mul_0_l. rewrite Nat.add_0_l.
@@ -631,6 +630,293 @@ Qed.
 
 
 
+
+
+
+Lemma tm_step_pred : forall (n k m : nat),
+    S (2*k) * 2^m < 2^n -> (
+    nth_error (tm_step n) (S (2*k) * 2^m)
+     = nth_error (tm_step n) (S (2*k) * 2^m - 1)
+     <-> odd m = true).
+Proof.
+  intros n k m.
+
+  generalize n. induction m. rewrite Nat.pow_0_r. rewrite Nat.mul_1_r.
+  destruct n0. rewrite Nat.pow_0_r. rewrite Nat.lt_1_r.
+  intro H. apply Nat.neq_succ_0 in H. contradiction H.
+  rewrite Nat.odd_0. rewrite Nat.sub_succ. rewrite Nat.sub_0_r.
+  rewrite <- tm_step_double_index. intro H. split. intro I.
+  symmetry in I. apply tm_step_succ_double_index in I. contradiction I.
+  apply Nat.lt_succ_l in H. rewrite Nat.pow_succ_r' in H.
+  rewrite <- Nat.mul_lt_mono_pos_l in H. assumption. apply Nat.lt_0_2.
+  intro I. apply diff_false_true in I. contradiction I.
+
+  intro n0. intro I.
+  destruct n0. rewrite Nat.pow_0_r in I. rewrite Nat.lt_1_r in I.
+  rewrite Nat.mul_eq_0 in I. destruct I.
+  apply Nat.neq_succ_0 in H. contradiction H.
+  apply Nat.pow_nonzero in H. contradiction H. easy.
+  rewrite Nat.pow_succ_r'. rewrite Nat.mul_assoc.
+  replace (S (2*k) * 2) with (2* (S (2*k))).
+  rewrite <- Nat.mul_assoc. rewrite <- tm_step_double_index.
+
+  (* réécriture de I *)
+  rewrite Nat.pow_succ_r' in I.
+  rewrite Nat.pow_succ_r' in I.
+  rewrite Nat.mul_assoc in I.
+  replace (S (2*k) * 2) with (2* (S (2*k))) in I.
+  rewrite <- Nat.mul_assoc in I.
+  rewrite <- Nat.mul_lt_mono_pos_l in I.
+  assert (J := I). apply IHm in J.
+
+  assert (M: 0 < 2^m). destruct m. simpl. apply Nat.lt_0_1.
+  replace (0) with (0 ^ (S m)) at 1.
+  apply Nat.pow_lt_mono_l. apply Nat.neq_succ_0. apply Nat.lt_0_2.
+  apply Nat.pow_0_l. apply Nat.neq_succ_0.
+
+  assert (L: S (2 * k) * 2 ^ m - 1 < S (2 * k) * 2 ^ m).
+  replace (S (2 * k) * 2 ^ m) with (S (S (2 * k) * 2 ^ m - 1)) at 2.
+  apply Nat.lt_succ_diag_r.
+  rewrite <- Nat.sub_succ_l. rewrite Nat.sub_1_r. rewrite pred_Sn.
+  reflexivity. rewrite Nat.le_succ_l. apply Nat.mul_pos_pos.
+  apply Nat.lt_0_succ. assumption.
+
+  assert (N: 2 * (S (2 * k) * 2 ^ m) - 1 < length (tm_step (S n0))).
+  rewrite tm_size_power2.
+  rewrite <- Nat.le_succ_l. rewrite <- Nat.add_1_r.
+  rewrite Nat.sub_add. rewrite Nat.pow_succ_r'.
+  rewrite <- Nat.mul_le_mono_pos_l.
+  apply Nat.lt_le_incl. assumption. apply Nat.lt_0_2.
+  apply Nat.le_succ_l. apply Nat.mul_pos_pos. apply Nat.lt_0_2.
+  apply Nat.mul_pos_pos. apply Nat.lt_0_succ.
+  assumption.
+
+  assert (nth_error (tm_step n0) ((S (2 * k) * 2 ^ m) - 1)
+    <> nth_error (tm_step (S n0)) (S (2 * (S (2 * k) * 2 ^ m - 1)))).
+  apply tm_step_succ_double_index.
+
+  generalize I. generalize L. apply Nat.lt_trans.
+
+  replace (S (2 * (S (2 * k) * 2 ^ m - 1))) with (2 * (S (2*k) * 2^m) - 1) in H.
+  rewrite Nat.odd_succ. rewrite <- Nat.negb_odd. destruct (odd m).
+
+  split. intro K. rewrite <- K in H.
+  destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m));
+  destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m - 1)).
+  destruct J. replace (Some b) with (Some b0) in H. contradiction H.
+  reflexivity. symmetry. apply H1. reflexivity.
+  destruct J. replace (Some b) with (None : option bool) in H.
+  contradiction H. reflexivity. symmetry. apply H1. reflexivity.
+  destruct J. replace (None : option bool) with (Some b) in H.
+  contradiction H. reflexivity. symmetry. apply H1. reflexivity.
+  contradiction H. reflexivity.
+
+  destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m));
+  destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m - 1)).
+  intro K. simpl in K. apply diff_false_true in K. contradiction K.
+  intro K. simpl in K. apply diff_false_true in K. contradiction K.
+  intro K. simpl in K. apply diff_false_true in K. contradiction K.
+  intro K. simpl in K. apply diff_false_true in K. contradiction K.
+
+  rewrite nth_error_nth' with (d := false) in J.
+  rewrite nth_error_nth' with (d := false) in J.
+  rewrite nth_error_nth' with (d := false) in H.
+  rewrite nth_error_nth' with (d := false) in H.
+  rewrite nth_error_nth' with (d := false).
+  rewrite nth_error_nth' with (d := false).
+  destruct (nth (S (2 * k) * 2 ^ m) (tm_step n0) false);
+  destruct (nth (S (2 * k) * 2 ^ m - 1) (tm_step n0) false);
+  destruct (nth (2 * (S (2 * k) * 2 ^ m) - 1) (tm_step (S n0)) false).
+  simpl; split; reflexivity.
+  destruct J. rewrite H0 in H. contradiction H. reflexivity.
+  reflexivity.
+  simpl; split; reflexivity. contradiction H. reflexivity.
+  contradiction H. reflexivity.
+  simpl; split; reflexivity.
+  destruct J. rewrite H0 in H. contradiction H. reflexivity.
+  reflexivity.
+  simpl; split; reflexivity.
+
+  assumption.
+  rewrite tm_size_power2. assumption.
+  assumption.
+  rewrite tm_size_power2. generalize I. generalize L.
+  apply Nat.lt_trans.
+  rewrite tm_size_power2. generalize I. generalize L.
+  apply Nat.lt_trans.
+  rewrite tm_size_power2. assumption.
+
+  rewrite Nat.mul_sub_distr_l. rewrite Nat.mul_1_r.
+  rewrite <- Nat.sub_succ_l. 
+  replace (S (2 * (S (2 * k) * 2 ^ m))) with (2 * (S (2 * k) * 2 ^ m) + 1).
+  rewrite <- Nat.add_cancel_r with (p := 1).
+  rewrite Nat.sub_add.
+
+
+
+
+
+
+
+
+
+  destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m));
+  destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m - 1));
+  destruct (nth_error (tm_step (S n0)) (2 * (S (2 * k) * 2 ^ m) - 1)).
+  destruct (b); destruct (b0); destruct (b1).
+  split. reflexivity. reflexivity.
+  destruct J. rewrite H0 in H. contradiction H. reflexivity.
+  reflexivity. simpl. split; reflexivity.
+  contradiction H. reflexivity. contradiction H. reflexivity.
+  simpl. split; reflexivity.
+  destruct J. rewrite H0 in H. contradiction H. reflexivity.
+  reflexivity. contradiction H. reflexivity.
+  destruct (b); destruct (b0). destruct J. rewrite H0.
+  split. intro J. inversion J. destruct H0. reflexivity.
+  intro J. simpl in J. symmetry in J. apply diff_false_true in J.
+  contradiction J. reflexivity.
+  split. intro K. inversion K.
+
+
+  apply Nat.lt_0_2. apply Nat.mul_comm.
+
+
+
+Lemma tm_step_repeating_patterns :
+  forall (n m i j : nat),
+  i < 2^m -> j < 2^m
+  -> forall k, k < 2^n -> nth_error (tm_step m) i
+                        = nth_error (tm_step m) j
+                      <-> nth_error (tm_step (m+n)) (k * 2^m + i)
+                        = nth_error (tm_step (m+n)) (k * 2^m + j).
+
+
+
+
+  induction m. rewrite Nat.pow_0_r. rewrite Nat.mul_1_r.
+  rewrite Nat.odd_0. rewrite Nat.sub_succ. rewrite Nat.sub_0_r.
+  destruct n. rewrite Nat.pow_0_r. rewrite Nat.lt_1_r.
+  intro H. apply Nat.neq_succ_0 in H. contradiction H.
+  rewrite <- tm_step_double_index. intro H. split. intro I.
+  symmetry in I. apply tm_step_succ_double_index in I. contradiction I.
+      apply Nat.lt_succ_l in H. rewrite Nat.pow_succ_r' in H.
+      rewrite <- Nat.mul_lt_mono_pos_l in H. assumption. apply Nat.lt_0_2.
+      intro I. apply diff_false_true in I. contradiction I.
+
+
+  intro H.
+  - induction m.
+    + rewrite Nat.pow_0_r. rewrite Nat.mul_1_r.
+      rewrite Nat.odd_0. rewrite Nat.sub_succ. rewrite Nat.sub_0_r.
+      destruct n. rewrite Nat.pow_0_r in H. rewrite Nat.mul_1_r in H.
+      rewrite Nat.lt_1_r in H. apply Nat.neq_succ_0 in H. contradiction H.
+      rewrite <- tm_step_double_index.
+      split.
+      intro I. symmetry in I.
+      apply tm_step_succ_double_index in I. contradiction I.
+      rewrite Nat.pow_0_r in H. rewrite Nat.mul_1_r in H.
+      apply Nat.lt_succ_l in H. rewrite Nat.pow_succ_r' in H.
+      rewrite <- Nat.mul_lt_mono_pos_l in H. assumption. apply Nat.lt_0_2.
+      intro I. apply diff_false_true in I. contradiction I.
+    +
+
+
+
+  split.
+  - induction m.
+    + rewrite Nat.pow_0_r. rewrite Nat.mul_1_r.
+      rewrite Nat.odd_0. rewrite Nat.sub_succ. rewrite Nat.sub_0_r.
+      destruct n. rewrite Nat.pow_0_r in H. rewrite Nat.mul_1_r in H.
+      rewrite Nat.lt_1_r in H. apply Nat.neq_succ_0 in H. contradiction H.
+      rewrite <- tm_step_double_index. intro I. symmetry in I.
+      apply tm_step_succ_double_index in I. contradiction I.
+      rewrite Nat.pow_0_r in H. rewrite Nat.mul_1_r in H.
+      apply Nat.lt_succ_l in H. rewrite Nat.pow_succ_r' in H.
+      rewrite <- Nat.mul_lt_mono_pos_l in H. assumption. apply Nat.lt_0_2.
+    +
+
+
+
+
+
+
+
+Theorem tm_step_stable : forall (n m k : nat),
+  k < 2^n -> k < 2^m -> nth_error (tm_step n) k = nth_error (tm_step m) k.
+Theorem tm_step_double_index : forall (n k : nat),
+  nth_error (tm_step n) k = nth_error (tm_step (S n)) (2*k).
+Theorem tm_step_succ_double_index : forall (n k : nat),
+  k < 2^n -> nth_error (tm_step n) k <> nth_error (tm_step (S n)) (S (2*k)).
+
+
+
+
+
+
+
+
+
+
+
+
+
+Require Import BinPosDef.
+Require Import BinNatDef.
+
+Lemma tm_step_double_index_pos : 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 (p~0)).
+Proof.
+  intro p.
+  simpl.
+
+
+
+
+Theorem tm_step_double_index : forall (n k : nat),
+  nth_error (tm_step n) k = nth_error (tm_step (S n)) (2*k).
+
+
+
+
+
+
+
+
+(*
+  From a(0) to a(2n+1), there are n+1 terms equal to 0 and n+1 terms equal to 1 (see Hassan Tarfaoui link, Concours Général 1990). - Bernard Schott, Jan 21 2022 
+   TODO Search "count_occ"
+ *)
+Theorem tm_step_count_occ : forall (hd tl : list bool) (k : nat),
+  tm_step k = hd ++ tl -> even (length hd) = true
+  -> count_occ Bool.bool_dec hd true = count_occ Bool.bool_dec hd false.
+Proof.
+  intros hd tl k. intros H I.
+  destruct k.
+  - assert (J: hd = nil). destruct hd. reflexivity.
+    simpl in H. inversion H.
+    symmetry in H2. apply app_eq_nil in H2.
+    destruct H2. rewrite H0 in I. simpl in I. inversion I.
+    rewrite J. reflexivity.
+  - rewrite <- tm_step_lemma in H.
+    generalize I. generalize H. induction hd.
+    reflexivity.
+
+
+
+    rewrite <- length_zero_iff_nil. simpl.
+    
+
+PeanoNat.Nat.neq_succ_0: forall n : nat, S n <> 0
+
+
+
+
+
+
+
+
+
   (* TODO: supprimer head_2 *)
 
 (* vérifier si les deux sont nécessaires *)
@@ -654,19 +940,12 @@ Definition hamming_weight_n (x: N) :=
   | Npos x => hamming_weight_positive x
   end.
 
-Lemma hamming_weight_remove_high : forall (x : N),
-  (0 < x)%N -> hamming_weight_n x = S (hamming_weight_n (x - 2^(N.log2 x))).
-Proof.
-  intros x.
 
 
 
 
 
 
-N.shiftl_spec_alt:
-  forall a n m : N, N.testbit (N.shiftl a n) (m + n) = N.testbit a m
-
 
 
 Lemma hamming_weight_positive_nonzero : forall (x: positive),