From 0e43274f90f179b008f47e24af7370f9eb0e0d41 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Thu, 29 Dec 2022 10:39:52 +0100 Subject: [PATCH] Update --- thue-morse.v | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/thue-morse.v b/thue-morse.v index 88bbc3f..d22196b 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -662,10 +662,7 @@ Proof. rewrite <- Nat.mul_lt_mono_pos_l in I. assert (J := I). apply IHm in J. - assert (M: 0 < 2^m). destruct m. simpl. apply Nat.lt_0_1. - replace (0) with (0 ^ (S m)) at 1. - apply Nat.pow_lt_mono_l. apply Nat.neq_succ_0. apply Nat.lt_0_2. - apply Nat.pow_0_l. apply Nat.neq_succ_0. + assert (M: 0 < 2^m). rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. assert (L: S (2 * k) * 2 ^ m - 1 < S (2 * k) * 2 ^ m). replace (S (2 * k) * 2 ^ m) with (S (S (2 * k) * 2 ^ m - 1)) at 2.