From 656fb217b14ba90e8e067b56260de7ed6cbc7136 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Wed, 28 Dec 2022 19:26:04 +0100 Subject: [PATCH] Update --- thue-morse.v | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/thue-morse.v b/thue-morse.v index 30530b5..bc6ccc6 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -746,8 +746,34 @@ Proof. apply Nat.lt_trans. rewrite tm_size_power2. assumption. + rewrite Nat.mul_sub_distr_l. rewrite Nat.mul_1_r. rewrite <- Nat.sub_succ_l. + rewrite Nat.sub_succ. reflexivity. + replace (2) with (2*1) at 1. + apply Nat.mul_le_mono_pos_l. apply Nat.lt_0_2. + apply Nat.le_succ_l. apply Nat.mul_pos_pos. + apply Nat.lt_0_succ. assumption. apply Nat.mul_1_r. + apply Nat.lt_0_2. + + apply Nat.mul_comm. + apply Nat.mul_comm. +Qed. + + + + + replace (S (2 * (S (2 * k) * 2 ^ m))) with (2 * (S (2 * k) * 2 ^ m) + 1). + rewrite <- Nat.add_cancel_r with (p := 1). + rewrite Nat.sub_add. rewrite <- Nat.add_sub_assoc. rewrite Nat.add_shuffle0. + rewrite <- Nat.add_assoc. + + + rewrite Nat.sub_succ. + rewrite <- Nat.add_cancel_r with (p := 1). + rewrite Nat.sub_add. rewrite <- Nat.add_assoc. + rewrite + replace (S (2 * (S (2 * k) * 2 ^ m))) with (2 * (S (2 * k) * 2 ^ m) + 1). rewrite <- Nat.add_cancel_r with (p := 1). rewrite Nat.sub_add.