diff --git a/src/thue_morse3.v b/src/thue_morse3.v
index 0b0c465..90a4a19 100644
--- a/src/thue_morse3.v
+++ b/src/thue_morse3.v
@@ -18,8 +18,14 @@ Lemma tm_step_palindromic_odd : forall (n : nat) (hd a tl : list bool),
   tm_step n = hd ++ a ++ tl
   -> a = rev a
   -> odd (length a) = true
-  -> length a <> 5.
+  -> length a < 4.
 Proof.
+  (* end of the lemma *)
+  assert (LEMMA: forall (n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ tl
+  -> a = rev a
+  -> odd (length a) = true
+  -> length a <> 5).
   intros n hd a tl. intros H I J.
   destruct a. easy. destruct a. easy.
   destruct a. easy. destruct a. easy.
@@ -87,14 +93,8 @@ Proof.
 
   simpl. apply not_eq_S. apply not_eq_S. apply not_eq_S.
   apply not_eq_S. apply not_eq_S. apply Nat.neq_succ_0.
-Qed.
+  (* end of the lemma *)
 
-Lemma tm_step_palindromic_odd' : forall (n : nat) (hd a tl : list bool),
-  tm_step n = hd ++ a ++ tl
-  -> a = rev a
-  -> odd (length a) = true
-  -> length a < 4.
-Proof.
   intros n hd a tl. intros H I J.
 
   assert (length a <= 5 \/ 5 < length a). apply Nat.le_gt_cases.
@@ -104,7 +104,7 @@ Proof.
   apply Nat.lt_eq_cases in H0. destruct H0. assumption.
   rewrite H0 in J. inversion J.
   assert (length a <> 5). generalize J. generalize I. generalize H.
-  apply tm_step_palindromic_odd. rewrite H0 in H1. contradiction H1.
+  apply LEMMA. rewrite H0 in H1. contradiction H1.
   reflexivity.
 
   (* main part of the proof:
@@ -201,6 +201,6 @@ Proof.
   assert (odd (length v) = true). rewrite H4. reflexivity.
   generalize H7. generalize H6. generalize H. rewrite H2.
   rewrite <- app_assoc. rewrite <- app_assoc. rewrite app_assoc.
-  apply tm_step_palindromic_odd. rewrite H4 in H7. contradiction H7.
+  apply LEMMA. rewrite H4 in H7. contradiction H7.
   reflexivity.
 Qed.