diff --git a/thue-morse.v b/thue-morse.v
index 5926fac..338465b 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -834,18 +834,9 @@ Qed.
 Lemma list_app_length_lt : forall (l l1 l2 : list bool) (b : bool),
   l = l1 ++ b :: l2 -> length l1 < length l.
 Proof.
-  intros l l1 l2 b. intros H.
-  assert (I: l = (l1 ++ b::nil) ++ l2).
-  { rewrite H. rewrite <- app_assoc. reflexivity. }
-  assert (J: length (l1 ++ b::nil) <= length l).
-  { rewrite I.
-    replace (length ((l1 ++ [b]) ++ l2)) with
-      (length (l1 ++ [b]) + length l2).
-      apply Nat.le_add_r.
-    symmetry. apply app_length. }
-  rewrite last_length in J. assert (L: length l1 < S (length l1)).
-    apply Nat.lt_succ_diag_r. generalize J. generalize L.
-    apply Nat.lt_le_trans.
+  intros l l1 l2 b. intros H. rewrite H.
+  rewrite app_length. simpl. apply Nat.lt_add_pos_r.
+  apply Nat.lt_0_succ.
 Qed.
 
 Lemma list_concat_to_pos : forall (l l1 l2 : list bool) (b : bool),
@@ -865,9 +856,9 @@ Lemma tm_step_next_range :
     -> nth_error (tm_step (S n)) (length l1) = Some b.
 Proof.
   intros n l1 l2 b. intros H.
-  assert (nth_error (tm_step n) (length l1) = Some b).
+  assert (I: nth_error (tm_step n) (length l1) = Some b).
   generalize H. apply list_concat_to_pos.
-  rewrite tm_build. rewrite nth_error_app1. apply H0.
+  rewrite tm_build. rewrite nth_error_app1. apply I.
   generalize H. apply list_app_length_lt.
 Qed.