From ba491a33d301b0c16b6b983e02e732e2cf1d0b30 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Wed, 28 Dec 2022 19:27:22 +0100 Subject: [PATCH] Update --- thue-morse.v | 7 ------- 1 file changed, 7 deletions(-) diff --git a/thue-morse.v b/thue-morse.v index 5fec985..809a78c 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -627,12 +627,6 @@ Proof. Qed. - - - - - - Lemma tm_step_pred : forall (n k m : nat), S (2*k) * 2^m < 2^n -> ( nth_error (tm_step n) (S (2*k) * 2^m) @@ -660,7 +654,6 @@ Proof. replace (S (2*k) * 2) with (2* (S (2*k))). rewrite <- Nat.mul_assoc. rewrite <- tm_step_double_index. - (* réécriture de I *) rewrite Nat.pow_succ_r' in I. rewrite Nat.pow_succ_r' in I. rewrite Nat.mul_assoc in I.