diff --git a/src/thue_morse3.v b/src/thue_morse3.v
index 9479d76..ead0c5b 100644
--- a/src/thue_morse3.v
+++ b/src/thue_morse3.v
@@ -1833,7 +1833,22 @@ Proof.
   apply Nat.le_refl.
 
 
-Admitted.
+
+  rewrite <- Nat.div_add. rewrite Nat.mul_comm.
+  replace (2 * Nat.div2 (length a'))
+    with (2 * Nat.div2 (length a') + Nat.b2n (Nat.odd (length a'))).
+  rewrite <- Nat.div2_odd. rewrite <- Nat.div2_div. reflexivity.
+  rewrite <- Nat.negb_even. rewrite J'. simpl. rewrite Nat.add_0_r.
+  reflexivity. easy. easy. rewrite Nat.div2_div. reflexivity.
+  rewrite Nat.mul_comm. simpl. rewrite Nat.add_0_r. reflexivity.
+  apply Nat.le_refl.
+  rewrite <- Nat.div_add. rewrite Nat.mul_comm.
+  replace (2 * Nat.div2 (length a))
+    with (2 * Nat.div2 (length a) + Nat.b2n (Nat.odd (length a))).
+  rewrite <- Nat.div2_odd. rewrite <- Nat.div2_div. reflexivity.
+  rewrite <- Nat.negb_even. rewrite J. simpl. rewrite Nat.add_0_r.
+  reflexivity. easy.
+Qed.