Update

src/thue_morse3.v

@@ -269,6 +269,16 @@ Proof.
   rewrite <- tm_build. reflexivity.
 Qed.
 
+(* very close to the previous one but we add the case n=0 here *)
+Theorem tm_step_palindromic_full_even : forall (n : nat),
+  even n = true -> tm_step n = rev (tm_step n).
+Proof.
+  intro n. intro H. destruct n. reflexivity.
+  rewrite Nat.even_succ in H. apply tm_step_palindromic_full in H.
+  rewrite H. rewrite rev_app_distr. rewrite rev_involutive.
+  reflexivity.
+Qed.
+
 (*
 Lemma tm_step_palindromic_full : forall (n : nat),
   tm_step (Nat.double (S n)) =