From 94c0e535effe7c1fde7492d269f7598d2f41a0a4 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Fri, 6 Jan 2023 14:25:35 +0100 Subject: [PATCH] Update --- src/thue_morse.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/thue_morse.v b/src/thue_morse.v index 93632a1..cc14b54 100644 --- a/src/thue_morse.v +++ b/src/thue_morse.v @@ -785,10 +785,9 @@ Proof. rewrite Nat.mul_comm. replace (2) with (2^1). replace (S (k*2^1)) with (k*2^1 + 2^0). apply tm_step_flip_low_bit. apply Nat.lt_0_1. - simpl. rewrite Nat.add_0_r. replace (k*2) with (k+k). + rewrite Nat.mul_comm. simpl. rewrite Nat.add_0_r. rewrite Nat.add_0_r. apply Nat.add_lt_mono; assumption. - rewrite Nat.mul_comm. simpl. rewrite Nat.add_0_r. reflexivity. - simpl. rewrite Nat.add_1_r. reflexivity. reflexivity. + simpl. rewrite Nat.add_1_r. reflexivity. apply Nat.pow_1_r. Qed.