From c2f9b2a0d58c372c119506ac02c2f51641099138 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Wed, 4 Jan 2023 17:58:57 +0100 Subject: [PATCH] Update --- src/thue_morse.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/thue_morse.v b/src/thue_morse.v index 736d8fd..15d7c6c 100644 --- a/src/thue_morse.v +++ b/src/thue_morse.v @@ -292,9 +292,8 @@ Theorem tm_step_negb : forall (n : nat), Proof. intro n. rewrite <- tm_step_lemma. symmetry. - replace (tm_step n) with (rev (rev (tm_step n))); rewrite rev_involutive. - - rewrite tm_morphism_rev. rewrite tm_build_negb. reflexivity. - - reflexivity. + rewrite tm_morphism_rev. rewrite tm_build_negb. rewrite rev_involutive. + reflexivity. Qed. Theorem tm_build : forall (n : nat),