From e84518300458175b5abb26b0b33c651bcf0f0610 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Wed, 4 Jan 2023 19:17:03 +0100 Subject: [PATCH] Update --- src/thue_morse.v | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/src/thue_morse.v b/src/thue_morse.v index 6e28a54..860d13f 100644 --- a/src/thue_morse.v +++ b/src/thue_morse.v @@ -1324,11 +1324,9 @@ Lemma tm_step_cube7 : forall (n : nat), /\ 0 < length b. Proof. intros n. intro H. - induction n. - - destruct H. destruct H. destruct H. destruct H. - exists x. exists x0. exists x1. split; assumption. - - destruct H. destruct H. destruct H. destruct H. - assert (J: exists (hd2 b2 tl2 : list bool), + induction n; destruct H; destruct H; destruct H; destruct H. + - exists x. exists x0. exists x1. split; assumption. + - assert (J: exists (hd2 b2 tl2 : list bool), tm_step (Nat.pred (S n)) = hd2 ++ b2 ++ b2 ++ b2 ++ tl2 /\ 0 < length b2). generalize H0. generalize H. apply tm_step_cube6.