From dd2bd9d4f59d3071f87550253320ddd0c68ab795 Mon Sep 17 00:00:00 2001
From: Thomas Baruchel <baruchel@gmx.com>
Date: Sat, 10 Dec 2022 22:32:51 +0100
Subject: [PATCH] Update

---
 thue-morse.v | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/thue-morse.v b/thue-morse.v
index 9a0bf58..b423ef0 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -1190,6 +1190,9 @@ Proof.
       generalize H2. generalize J. apply Nat.le_trans.
 Qed.
 
+(* Note: a first version included the  0 < k  hypothesis but in the very
+   unorthodox case where k=0 it happens to be true anyway, and the hypothesis
+   was removed in order to make the theorem more general *)
 Theorem tm_step_flip_low_bit :
   forall (n m k j : nat),
   j < m -> k * 2^m < 2^n
@@ -1212,8 +1215,7 @@ Proof.
   rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
   apply Nat.le_0_l. assumption.
 
-  assert (G: k = 0 \/ 0 < k). apply Nat.eq_0_gt_0_cases.
-  destruct G.
+  assert (G: k = 0 \/ 0 < k). apply Nat.eq_0_gt_0_cases. destruct G.
 
   (* k = 0 *)
   rewrite H0. rewrite Nat.mul_0_l. rewrite Nat.add_0_l.