From 358404d2be488c2fd5b53024d81b80efe6c33f8a Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Sun, 22 Jan 2023 22:28:24 +0100 Subject: [PATCH] Update --- src/thue_morse3.v | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/thue_morse3.v b/src/thue_morse3.v index e2c21d0..21166ec 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -949,8 +949,14 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM : simpl. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ. - unfold lh. - + rewrite Nat.mul_lt_mono_pos_l with (p := 8). + rewrite Nat.add_lt_mono_r with (p := 2). rewrite <- H9. + rewrite Nat.add_lt_mono_r with (p := 8). + rewrite <- Nat.add_sub_swap. rewrite Nat.add_sub. + rewrite <- Nat.add_assoc. replace (2+8) with 10. + replace (8) with (2^3) at 1. rewrite <- Nat.pow_add_r. + rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap. simpl. +