From e0754cb433f5727c1dbeb408025930cfdc80ca30 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Wed, 23 Nov 2022 09:15:58 +0100 Subject: [PATCH] Update --- thue-morse.v | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/thue-morse.v b/thue-morse.v index 497aca2..5926fac 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -867,10 +867,8 @@ Proof. intros n l1 l2 b. intros H. assert (nth_error (tm_step n) (length l1) = Some b). generalize H. apply list_concat_to_pos. - rewrite tm_build. - assert (length l1 < length (tm_step n)). - generalize H. apply list_app_length_lt. - rewrite nth_error_app1. apply H0. apply H1. + rewrite tm_build. rewrite nth_error_app1. apply H0. + generalize H. apply list_app_length_lt. Qed. Lemma tm_step_next_range' :