From f6d6f3f693f452c6ebbc5d516a69f907f1356ad4 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Tue, 13 Dec 2022 13:50:33 +0100 Subject: [PATCH] Update --- thue-morse.v | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/thue-morse.v b/thue-morse.v index ebfcc62..1ca36f9 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -1231,6 +1231,7 @@ Proof. assert (O: k*2^m + 2^j < 2^n). apply lt_split_bits. assumption. assumption. assumption. + assert (P: 2^n <= 2^(m+n)). apply Nat.pow_le_mono_r. easy. apply Nat.le_add_l. assert ( nth_error (tm_step m) 0 = nth_error (tm_step m) (2^j) @@ -1265,14 +1266,12 @@ Proof. apply H1 in H2. rewrite H2 at 1. easy. easy. rewrite nth_error_nth' with (d := false). easy. rewrite tm_size_power2. assumption. - apply tm_step_stable. assumption. - - assert (2^n <= 2^(m+n)). apply Nat.pow_le_mono_r. easy. apply Nat.le_add_l. - generalize H1. generalize O. apply Nat.lt_le_trans. apply tm_step_stable. assumption. - assert (2^n <= 2^(m+n)). apply Nat.pow_le_mono_r. easy. apply Nat.le_add_l. - generalize H1. generalize I. apply Nat.lt_le_trans. + generalize P. generalize O. apply Nat.lt_le_trans. + + apply tm_step_stable. assumption. + generalize P. generalize I. apply Nat.lt_le_trans. Qed.