diff --git a/src/thue_morse3.v b/src/thue_morse3.v
index 86b235c..946dfc5 100644
--- a/src/thue_morse3.v
+++ b/src/thue_morse3.v
@@ -2456,7 +2456,6 @@ Proof.
 
   reflexivity.
 
-
   rewrite Nat.mul_comm. replace (2^3) with 8.
   replace 4 with (length (hd++a) mod 8) at 3.
   rewrite <- Nat.div_mod_eq. rewrite <- H0 at 1.
@@ -2471,10 +2470,13 @@ Proof.
   rewrite <- app_assoc. reflexivity. reflexivity.
 
   rewrite H2 in H1. rewrite H3 in H1. simpl in H1.
-  inversion H1. contradiction H4.
-
-
+  destruct H1. assert (Some false = Some true).
+  apply H4. reflexivity. inversion H5.
 
+  rewrite Nat.add_comm.
+  rewrite Nat.sub_add. reflexivity.
+  apply Nat.lt_le_incl. assumption.
+Qed.