From 27b630570b1a962355b6ca870be904fd750b155e Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Sun, 22 Jan 2023 17:45:16 +0100 Subject: [PATCH] Update --- src/thue_morse3.v | 1 + 1 file changed, 1 insertion(+) diff --git a/src/thue_morse3.v b/src/thue_morse3.v index feb87b3..a17abc7 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -860,6 +860,7 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM : rewrite e0 in H7. inversion H7. assumption. easy. + assert (V: nth_error (b4 :: b6 :: b9 :: tl) 2 = Some b9). reflexivity. False, True, True, False, True, False, False, True, True, False, False