Update

src/thue_morse4.v

@@ -28,6 +28,7 @@ Theorem tm_step_palindrome_power2_inverse :
     -> skipn (length hd - 2^m) hd = rev (firstn (2^m) tl).
 Proof.
   intros m n k hd tl. intros H I J K.
+
   assert (L: 2^m <= length hd). rewrite I. lia.
   assert (M: m < n). assert (length (tm_step n) = length (hd ++ tl)).
   rewrite H. reflexivity. rewrite tm_size_power2 in H0.
@@ -121,3 +122,42 @@ Proof.
   - rewrite firstn_skipn. reflexivity.
   - rewrite firstn_skipn. reflexivity.
 Qed.
+
+
+
+
+Theorem tm_step_palindrome_power2_inverse' :
+  forall (m n k : nat) (hd tl : list bool),
+    tm_step n = hd ++ tl
+    -> length hd = S (Nat.double k) * 2^m
+    -> odd m = true
+    -> 0 < k
+    -> skipn (length hd - 2^m) hd = rev (firstn (2^m) tl).
+Proof.
+  intros m n k hd tl. intros H I J L.
+
+  assert (K: {tl=nil} + {~ tl=nil}). apply list_eq_dec. apply bool_dec.
+  destruct K as [K|K]. rewrite K in H. rewrite app_nil_r in H.
+  rewrite <- H in I. rewrite tm_size_power2 in I.
+
+  assert (n <= m \/ m < n). apply Nat.le_gt_cases. destruct H0.
+  apply Nat.pow_le_mono_r with (a := 2) in H0. rewrite I in H0.
+  rewrite <- Nat.mul_1_l in H0. rewrite <- Nat.mul_le_mono_pos_r in H0.
+  rewrite <- Nat.succ_le_mono in H0. apply Nat.le_0_r in H0.
+  rewrite Nat.double_twice in H0. apply Nat.mul_eq_0_r in H0.
+  rewrite H0 in L. inversion L. easy.
+  rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. easy.
+  replace n with (n-m+m) in I. rewrite Nat.pow_add_r in I.
+  rewrite Nat.mul_cancel_r in I.
+
+  assert (even (2^(n-m)) = true). apply Nat.sub_gt in H0.
+  apply Nat.neq_0_lt_0 in H0. destruct (n-m). inversion H0.
+  rewrite Nat.pow_succ_r. rewrite Nat.even_mul. reflexivity.
+  apply Nat.le_0_l. rewrite I in H1. rewrite Nat.even_succ in H1.
+  rewrite Nat.double_twice in H1. rewrite Nat.odd_mul in H1.
+  inversion H1. apply Nat.pow_nonzero. easy. lia.
+
+  generalize K. generalize J. generalize I. generalize H.
+  apply tm_step_palindrome_power2_inverse.
+Qed.
+