From 5399610d21172e6c1836fa9f5ba985af62701c71 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Sat, 26 Nov 2022 07:54:06 +0100 Subject: [PATCH] Update --- thue-morse.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thue-morse.v b/thue-morse.v index 9da7180..cd4cfba 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -1100,7 +1100,7 @@ Proof. assert (2^n < 2^(S n)). apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. apply Nat.lt_succ_diag_r. generalize H1. generalize H0. apply Nat.lt_trans. rewrite <- H1. - rewrite tm_step_repunit_index. + rewrite tm_step_repunit_index. destruct (odd n). easy. easy. rewrite Nat.succ_lt_mono. simpl. (*