From b0e15fc10a06a4adfffcd1769b9fbd6a7a8c2495 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Sat, 26 Nov 2022 06:45:16 +0100 Subject: [PATCH] Update --- thue-morse.v | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/thue-morse.v b/thue-morse.v index 5595126..7396b83 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -830,7 +830,21 @@ Proof. reflexivity. Qed. -Lemma tm_step_repunit : forall (n : nat), + +Lemma tm_step_single_bit_index : forall (n : nat), + nth_error (tm_step (S n)) (2^n) = Some true. +Proof. + intros n. + induction n. + - simpl. reflexivity. + - rewrite tm_build. + rewrite nth_error_app2. rewrite tm_size_power2. rewrite Nat.sub_diag. + replace (true) with (negb false). apply map_nth_error. + rewrite tm_step_head_1. simpl. reflexivity. + 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. intros n.