diff --git a/thue-morse.v b/thue-morse.v
index 5c800bf..47a9065 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -1107,22 +1107,52 @@ Lemma lt_even_even : forall (a b : nat),
   even a = true -> even b = true -> a < b -> S a < b.
 Proof.
   intros a b. intros H I J.
-  assert (even (S a) = false). rewrite Nat.even_succ.
-  rewrite <- Nat.negb_odd in H. rewrite Bool.negb_true_iff in H. apply H.
-  assert (S a <> b).
-
-
-  assert (S (S a) <= b).
-
-
+  rewrite <- Nat.le_succ_l in J. rewrite Nat.lt_eq_cases in J.
+  destruct J.
+  - apply H0.
+  - rewrite <- H0 in I. rewrite Nat.even_succ in I.
+    rewrite <- I in H. rewrite <- Nat.negb_even in H.
+    destruct (even a).
+    + simpl in H. apply Bool.diff_true_false in H. contradiction H.
+    + simpl in H. symmetry in H. apply Bool.diff_true_false in H. contradiction H.
+Qed.
 
+Require Import Arith_prebase.
 
 Lemma tm_step_add_small_power :
   forall (n m k j : nat),
-  k * 2^m < 2^n -> j < m
+  1 < k -> k * 2^m < 2^n -> j < m
   -> nth_error (tm_step n) (k * 2^m) <> nth_error (tm_step n) (k * 2^m + 2^j).
 Proof.
-  intros n m k j. intros H I.
+  intros n m k j. intros J H I.
+
+  assert (M: 0 < m-j). rewrite Nat.add_lt_mono_l with (p := j).
+  rewrite Arith_prebase.le_plus_minus_r_stt. rewrite Nat.add_0_r. apply I.
+  generalize I. apply Nat.lt_le_incl.
+
+
+  (*
+        destruct (m-j). apply Nat.lt_irrefl in M. contradiction M.
+        rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_2.
+        simpl. rewrite Bool.orb_true_r. reflexivity. apply Nat.le_0_l.
+   *)
+  (*
+   *)
+
+  (*
+        assert (0 < n-m).
+        rewrite Nat.add_lt_mono_l with (p := m).
+        rewrite Arith_prebase.le_plus_minus_r_stt. rewrite Nat.add_0_r. apply H4.
+        generalize H4. apply Nat.lt_le_incl.
+   *)
+
+  (*
+  assert (N: 0 < n-j). rewrite Nat.add_lt_mono_l with (p := j).
+  rewrite Arith_prebase.le_plus_minus_r_stt. rewrite Nat.add_0_r.
+  generalize I. generalize I. apply Nat.lt_trans.
+  apply Nat.lt_le_incl. generalize H4. generalize I. apply Nat.lt_trans.
+   *)
+
 
   induction n.
   - simpl. destruct k.
@@ -1141,19 +1171,87 @@ Proof.
   - rewrite tm_build.
     assert (S: k * 2^m < 2^n \/ 2^n <= k * 2^m). apply Nat.lt_ge_cases.
     destruct S.
-    + rewrite nth_error_app1. rewrite nth_error_app1.
+    +
+      (* m < n *)
+      assert (N: m < n). apply Nat.lt_le_incl in H0.
+      apply Nat.log2_le_mono in H0.
+      rewrite Nat.log2_mul_pow2 in H0. rewrite Nat.log2_pow2 in H0.
+      generalize H0. assert (m < m + Nat.log2 k).
+      apply Nat.lt_add_pos_r. apply Nat.log2_pos. apply J.
+      generalize H1. apply Nat.lt_le_trans.
+      apply Nat.le_0_l. apply Nat.lt_succ_l in J. apply J.
+      apply Nat.le_0_l.
+
+      assert (0 < n-m).
+      rewrite Nat.add_lt_mono_l with (p := m).
+      rewrite Arith_prebase.le_plus_minus_r_stt. rewrite Nat.add_0_r. apply N.
+      generalize N. apply Nat.lt_le_incl.
+
+      assert (0 < n-j). rewrite Nat.add_lt_mono_l with (p := j).
+      rewrite Arith_prebase.le_plus_minus_r_stt. rewrite Nat.add_0_r.
+      generalize N. generalize I. apply Nat.lt_trans.
+      apply Nat.lt_le_incl. generalize N. generalize I. apply Nat.lt_trans.
+
+      rewrite nth_error_app1. rewrite nth_error_app1.
       apply IHn. apply H0. rewrite tm_size_power2.
 
       replace (k*2^m + 2^j < 2^n) with ((k*2^(m-j)+1)*(2^j) < 2^(n-j)*2^j).
       apply Nat.mul_lt_mono_pos_r.
       rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
 
+      assert (0 < m). assert (0 <= j). apply Nat.le_0_l.
+      generalize I. generalize H3. apply Nat.le_lt_trans.
+
+      assert (0 < n). destruct k. apply Nat.nlt_succ_diag_l in J. contradiction J.
+      assert (2^0 <= (S k) * (2^m)). simpl. assert (1 <= 2^m).
+      replace (1) with (2^0) at 1. apply Nat.pow_le_mono_r. easy.
+      apply Nat.le_0_l. reflexivity.
+      generalize H4. apply Arith_prebase.le_plus_trans_stt.
+      assert (2^0 < 2^n). generalize H0. generalize H4.
+      apply Nat.le_lt_trans. rewrite <- Nat.pow_lt_mono_r_iff in H5.
+      apply H5. apply Nat.lt_1_2.
+
+      assert (S (k*2^m) < 2^n). apply lt_even_even.
+      rewrite Nat.even_mul.
+
+      assert (Nat.even (2^m) = true). destruct m.
+      * apply Nat.lt_irrefl in H3. contradiction H3.
+      * rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_2.
+        reflexivity. apply Nat.le_0_l.
+      * destruct m. apply Nat.lt_irrefl in H3. contradiction H3.
+        rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_2.
+        simpl. rewrite Bool.orb_true_r. reflexivity. apply Nat.le_0_l.
+      * destruct m. apply Nat.lt_irrefl in H3. contradiction H3.
+
+        destruct n.
+        apply Nat.lt_irrefl in H2. contradiction H2.
+        rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_2.
+        reflexivity. apply Nat.le_0_l.
+      * apply H0.
+      * rewrite Nat.add_1_r. apply lt_even_even. rewrite Nat.even_mul.
+
+        destruct (m-j). apply Nat.lt_irrefl in M. contradiction M.
+        rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_2.
+        simpl. rewrite Bool.orb_true_r. reflexivity. apply Nat.le_0_l.
+
+        destruct (n-j). apply Nat.lt_irrefl in H2. contradiction H2.
+        rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_2.
+        reflexivity. apply Nat.le_0_l.
+
+        apply Nat.mul_lt_mono_pos_r with (p := 2^j).
+        rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
 
 
-Nat.shiftl_mul_pow2: forall a n : nat, Nat.shiftl a n = a * 2 ^ n
-
+        rewrite <- Nat.pow_add_r.
+        rewrite <- Nat.mul_assoc. rewrite <- Nat.pow_add_r.
 
+        rewrite Nat.sub_add. rewrite Nat.sub_add.
+        apply H0.
 
+        apply Nat.lt_le_incl.
+        generalize N. generalize I. apply Nat.lt_trans.
+        apply Nat.lt_le_incl. apply I.
+      *