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 *)