Update

2022-11-26 07:54:12 +01:00 · 2022-11-26 07:54:06 +01:00
1 changed files with 1 additions and 2 deletions
--- a/thue-morse.v
+++ b/thue-morse.v
@ -1100,9 +1100,8 @@ Proof.
  assert (2^n < 2^(S n)). apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
  apply Nat.lt_succ_diag_r.
  generalize H1. generalize H0. apply Nat.lt_trans. rewrite <- H1.
-  rewrite tm_step_repunit_index.
+  rewrite tm_step_repunit_index. destruct (odd n). easy. easy.

-  rewrite Nat.succ_lt_mono. simpl.
  (*
  assert (K: nth_error (tm_step n) a = Some (odd n)). rewrite I.
  apply tm_step_repunit.
Author	SHA1	Message	Date
Thomas Baruchel	a93c2a6607	Update	2022-11-26 07:54:12 +01:00
Thomas Baruchel	5399610d21	Update	2022-11-26 07:54:06 +01:00