From 8a04d818b7b87789f24213a1b7d67592a17b1cb8 Mon Sep 17 00:00:00 2001
From: Thomas Baruchel <baruchel@gmx.com>
Date: Wed, 7 Dec 2022 21:29:26 +0100
Subject: [PATCH] Update

---
 thue-morse.v | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/thue-morse.v b/thue-morse.v
index e0d11dd..775986f 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -1193,8 +1193,15 @@ Proof.
     rewrite <- Nat.pow_add_r. rewrite Nat.sub_add. reflexivity.
     apply Nat.lt_le_incl. apply N5.
     apply Nat.lt_le_incl. apply I.
-  - assert ((S k)*2^m + 2^j < 2^(S n)).
+  - assert ((S k)*2^m + 2^j < 2^(S n)). rewrite Nat.add_comm.
     apply Nat.add_lt_mono with (p := 2^m) (q := 2^n) in O.
+    rewrite <- Nat.add_assoc in O. rewrite Nat.add_shuffle3 in O.
+    replace (2^m) with (1 * 2^m) in O at 2. rewrite <- Nat.mul_add_distr_r in O.
+    rewrite Nat.add_1_r in O. rewrite Nat.pow_succ_r'.
+    replace (2^n) with (1*2^n) in O. rewrite <- Nat.mul_add_distr_r in O.
+    rewrite Nat.add_1_r in O. apply O.
+    rewrite Nat.mul_1_l. reflexivity. rewrite Nat.mul_1_l. reflexivity.
+    apply N0.