From 1aea07ca1f18ce5d684df8d8cad17fb2ff6c8ef7 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Sun, 22 Jan 2023 22:42:58 +0100 Subject: [PATCH] Update --- src/thue_morse3.v | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/thue_morse3.v b/src/thue_morse3.v index d398bb4..7e9ba36 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -966,7 +966,10 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM : apply Nat.lt_0_succ. apply Nat.le_refl. apply Nat.lt_le_incl. assumption. reflexivity. reflexivity. assumption. apply Nat.lt_0_succ. - + apply Nat.div_le_mono with (c := 8) in T. rewrite Nat.div_same in T. + rewrite Nat.le_succ_l in T. assumption. easy. easy. + + (* on change de modulo ; on travaille sur 8k+6 maintenant *)