From a12c0e3fd273f4f5b1fcdd0e8e878b3272b6ec1f Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Sun, 22 Jan 2023 21:36:25 +0100 Subject: [PATCH] Update --- src/thue_morse3.v | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) diff --git a/src/thue_morse3.v b/src/thue_morse3.v index 647eef6..78a9b83 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -921,7 +921,7 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM : rewrite <- Nat.add_succ_comm. rewrite <- Nat.add_succ_comm. rewrite <- Nat.add_succ_comm. rewrite app_length in T. assumption. reflexivity. rewrite Y''. -rewrite app_length. + rewrite app_length. replace (length (b3::b5::b7::hd)) with (S (S (S (length hd)))). rewrite Nat.add_succ_comm. rewrite Nat.add_succ_comm. rewrite Nat.add_succ_comm. rewrite <- Nat.sub_succ_l. @@ -930,7 +930,22 @@ rewrite app_length. rewrite Nat.add_succ_r. rewrite Nat.add_succ_r. rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. replace 5 with (1 + 4). - rewrite <- Nat.add_le_mono_r. + rewrite <- Nat.add_le_mono_r. destruct hd. inversion Q. + simpl. apply le_n_S. apply le_0_n. reflexivity. reflexivity. + rewrite Y''. rewrite app_length. + replace (length (b3::b5::b7::hd)) with (S (S (S (length hd)))). + rewrite Nat.add_succ_comm. rewrite Nat.add_succ_comm. + rewrite Nat.add_succ_comm. rewrite <- Nat.sub_succ_l. + rewrite <- Nat.add_succ_r. rewrite Nat.add_sub. apply Nat.le_refl. + rewrite Nat.add_succ_r. rewrite Nat.add_succ_r. rewrite Nat.add_succ_r. + rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. + rewrite <- Nat.succ_le_mono. replace 5 with (1 + 4). + rewrite <- Nat.add_le_mono_r. destruct hd. inversion Q. + simpl. apply le_n_S. apply le_0_n. reflexivity. reflexivity. + apply Nat.lt_le_incl. assumption. + + +