From ea8e07d20d7b6e5dfb4e499053231f13f4d56265 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Thu, 29 Dec 2022 10:45:51 +0100 Subject: [PATCH] Update --- thue-morse.v | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/thue-morse.v b/thue-morse.v index d22196b..162ed78 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -681,11 +681,14 @@ Proof. apply Nat.mul_pos_pos. apply Nat.lt_0_succ. assumption. + assert(T: S (2 * k) * 2 ^ m - 1 < 2 ^ n0). + generalize I. generalize L. apply Nat.lt_trans. + assert (nth_error (tm_step n0) ((S (2 * k) * 2 ^ m) - 1) <> nth_error (tm_step (S n0)) (S (2 * (S (2 * k) * 2 ^ m - 1)))). apply tm_step_succ_double_index. - generalize I. generalize L. apply Nat.lt_trans. + assumption. replace (S (2 * (S (2 * k) * 2 ^ m - 1))) with (2 * (S (2*k) * 2^m) - 1) in H. rewrite Nat.odd_succ. rewrite <- Nat.negb_odd. destruct (odd m). @@ -728,8 +731,8 @@ Proof. simpl; split; reflexivity. assumption. rewrite tm_size_power2. assumption. assumption. - rewrite tm_size_power2. generalize I. generalize L. apply Nat.lt_trans. - rewrite tm_size_power2. generalize I. generalize L. apply Nat.lt_trans. + rewrite tm_size_power2. assumption. + rewrite tm_size_power2. assumption. rewrite tm_size_power2. assumption. rewrite Nat.mul_sub_distr_l. rewrite Nat.mul_1_r.