From a93c2a6607080e6fde066ce33958a48167f2c5be Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Sat, 26 Nov 2022 07:54:12 +0100 Subject: [PATCH] Update --- thue-morse.v | 1 - 1 file changed, 1 deletion(-) diff --git a/thue-morse.v b/thue-morse.v index cd4cfba..9800b77 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -1102,7 +1102,6 @@ Proof. generalize H1. generalize H0. apply Nat.lt_trans. rewrite <- H1. rewrite tm_step_repunit_index. destruct (odd n). easy. easy. - rewrite Nat.succ_lt_mono. simpl. (* assert (K: nth_error (tm_step n) a = Some (odd n)). rewrite I. apply tm_step_repunit.