From b830335fead87854abf3e530181a7832b1f74d09 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Tue, 22 Nov 2022 18:37:07 +0100 Subject: [PATCH] Update --- thue-morse.v | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/thue-morse.v b/thue-morse.v index 782cd05..de222ac 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -869,15 +869,13 @@ Proof. rewrite H1. easy. rewrite nth_error_Some in I. rewrite tm_size_power2 in I. assert (2^k <= length l1 + 2^k). - apply Nat.le_add_l. - generalize I. generalize H3. - apply Nat.le_lt_trans. + apply Nat.le_add_l. generalize I. generalize H3. apply Nat.le_lt_trans. } - assert (k < n). { - generalize H3. apply Nat.pow_lt_mono_r_iff. + assert (k < n). { generalize H3. apply Nat.pow_lt_mono_r_iff. + apply Nat.lt_succ_diag_r. } + - BEFORE REPLACEMENT.