diff --git a/src/thue_morse3.v b/src/thue_morse3.v
index b289016..39996b4 100644
--- a/src/thue_morse3.v
+++ b/src/thue_morse3.v
@@ -425,6 +425,7 @@ Proof.
   rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
   generalize Z. generalize H3. apply Nat.lt_trans.
 
+  (* FIRST PART OF THE PROOF: case b0 = b1 *)
   (* première hypothèse   b0 = b1 mais alors on construit vers la
      gauche jusqu'à  (lest hd) et l'on a dans l'ordre jusqu'au centre :
        b1 | (negb b1) b1 | b1 (negb b1  ||
@@ -580,7 +581,9 @@ Proof.
   apply tm_step_cubefree in H. contradiction H. reflexivity.
   apply Nat.lt_0_succ. reflexivity. easy. easy.
 
-
+  (* SECOND PART PF THE PROOF: case b0 <> b1 *)
+  assert ({b=b1} + {~ b=b1}). apply bool_dec. destruct H1.
+  rewrite e in H.