From ccc12a619c0628cc1cc7d1a173178e74ef7d2de7 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Sat, 10 Dec 2022 15:04:56 +0100 Subject: [PATCH] Update --- thue-morse.v | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/thue-morse.v b/thue-morse.v index f190a16..a1a68f6 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -1378,9 +1378,7 @@ Proof. rewrite tm_size_power2. apply lt_split_bits. assumption. assumption. assumption. replace (nth_error (tm_step m) (2^j)) with (nth_error (tm_step (S j)) (2^j)). - rewrite tm_build. rewrite nth_error_app2. rewrite tm_size_power2. - rewrite Nat.sub_diag. rewrite tm_step_head_1. simpl. reflexivity. - rewrite tm_size_power2. apply Nat.le_refl. + rewrite tm_step_single_bit_index. reflexivity. apply tm_step_stable. rewrite <- Nat.mul_1_l at 1. rewrite Nat.pow_succ_r. rewrite <- Nat.mul_lt_mono_pos_r. apply Nat.lt_1_2.