From 443008fbb5a50f7f3c72d8ab335a133d6b22d676 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Wed, 4 Jan 2023 14:42:31 +0100 Subject: [PATCH] Update --- thue-morse.v | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/thue-morse.v b/thue-morse.v index 27e9c4c..1741d1c 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -384,13 +384,6 @@ Proof. rewrite rev_length. assumption. apply rev_involutive. assumption. Qed. -Lemma list_app_length_lt : forall (l l1 l2 : list bool) (b : bool), - l = l1 ++ b :: l2 -> length l1 < length l. -Proof. - intros l l1 l2 b. intro H. rewrite H. - rewrite app_length. simpl. apply Nat.lt_add_pos_r. - apply Nat.lt_0_succ. -Qed. Lemma tm_step_next_range : forall (n k : nat) (b : bool), @@ -399,7 +392,8 @@ Proof. intros n k b. intro H. assert (I := H). apply nth_error_split in H. destruct H. destruct H. inversion H. rewrite tm_build. rewrite nth_error_app1. apply I. - apply list_app_length_lt in H0. rewrite H1 in H0. apply H0. + rewrite H0. rewrite app_length. rewrite <- H1. simpl. + apply Nat.lt_add_pos_r. apply Nat.lt_0_succ. Qed. Lemma tm_step_add_range : forall (n m k : nat),