From 8065518a98f67467c0ebe866c5ccaf6b27b45dd3 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Thu, 15 Dec 2022 15:41:36 +0100 Subject: [PATCH] Update --- thue-morse.v | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/thue-morse.v b/thue-morse.v index c8045d6..00da028 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -202,21 +202,20 @@ Proof. reflexivity. rewrite tm_size_power2. easy. Qed. - Lemma tm_step_repunit_index : forall (n : nat), nth_error (tm_step n) (2^n - 1) = Some (odd n). Proof. intro n. + assert (H: 2 ^ n - 1 < length (tm_step n)). rewrite tm_size_power2. + rewrite Nat.sub_1_r. apply Nat.lt_pred_l. apply Nat.pow_nonzero. easy. + rewrite nth_error_nth' with (d := false). replace (tm_step n) with (rev (rev (tm_step n))). rewrite rev_nth. rewrite rev_length. rewrite tm_size_power2. rewrite Nat.sub_1_r. rewrite Nat.succ_pred_pos. rewrite Nat.sub_diag. rewrite tm_step_end_1. reflexivity. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. - rewrite rev_length. rewrite tm_size_power2. - rewrite Nat.sub_1_r. apply Nat.lt_pred_l. apply Nat.pow_nonzero. easy. - apply rev_involutive. rewrite tm_size_power2. - rewrite Nat.sub_1_r. apply Nat.lt_pred_l. apply Nat.pow_nonzero. easy. + rewrite rev_length. assumption. apply rev_involutive. assumption. Qed. Lemma list_app_length_lt : forall (l l1 l2 : list bool) (b : bool),