From 5f373c7859ef3bc4128428aba63253f9d52c973e Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Sat, 10 Dec 2022 23:08:37 +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 ebd2aa8..b0eec01 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -1225,7 +1225,7 @@ Proof. rewrite H1. easy. easy. rewrite Nat.le_succ_l in H1. apply Nat.pow_lt_mono_r with (a := 2) in H1. rewrite tm_step_stable with (m := m). rewrite N. easy. assumption. assumption. - apply Nat.lt_1_2. rewrite tm_step_head_1. simpl. reflexivity. + apply Nat.lt_1_2. rewrite tm_step_head_1. reflexivity. (* k < 0 *) rename H0 into G.