From 85418e959b0efd211d7caead985786120211feed Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Thu, 15 Dec 2022 16:03:55 +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 00da028..bb4a54b 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -614,7 +614,21 @@ Proof. generalize P. generalize I. apply Nat.lt_le_trans. Qed. - +Lemma tm_step_succ_double_index : forall (n k : nat), + 2 * k < 2^n -> nth_error (tm_step n) k <> nth_error (tm_step n) (S (2*k)). +Proof. + intros n k. intro H. rewrite tm_step_double_index. + replace (nth_error (tm_step (S n)) (2*k)) with (nth_error (tm_step n) (2*k)). + rewrite Nat.mul_comm. replace (2) with (2^1). + replace (S (k*2^1)) with (k*2^1 + 2^0). + apply tm_step_flip_low_bit. apply Nat.lt_0_1. + simpl. rewrite Nat.mul_comm. assumption. + rewrite Nat.add_1_r. reflexivity. easy. + apply tm_step_stable. assumption. + assert (2^n < 2^(S n)). apply Nat.pow_lt_mono_r. + apply Nat.lt_1_2. apply Nat.lt_succ_diag_r. + generalize H0. generalize H. apply Nat.lt_trans. +Qed.