From c067e31ecd552698d477f76df3177fb8d66dcd59 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Mon, 23 Jan 2023 21:10:50 +0100 Subject: [PATCH] Update --- src/thue_morse3.v | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/thue_morse3.v b/src/thue_morse3.v index d23cb05..22433e3 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -1134,7 +1134,12 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM : simpl in Q. rewrite Q in H10. inversion H10. rewrite Y''. apply Nat.le_pred_l. (* now we know that b12 <> b1 *) - + (* proof that b12 = b0 *) + assert (b12 = b0). destruct b12; destruct b1; destruct b0. + reflexivity. contradiction n8. reflexivity. reflexivity. + contradiction n1. reflexivity. contradiction n1. reflexivity. + reflexivity. contradiction n8. reflexivity. reflexivity. + rewrite H10 in H.