From 46829e78a1441f8cd1ceedfacc228669769aeaf9 Mon Sep 17 00:00:00 2001
From: Thomas Baruchel <baruchel@gmx.com>
Date: Fri, 25 Nov 2022 14:21:36 +0100
Subject: [PATCH] Update

---
 thue-morse.v | 89 +++++++++++++++++-----------------------------------
 1 file changed, 29 insertions(+), 60 deletions(-)

diff --git a/thue-morse.v b/thue-morse.v
index 8f50bfb..e42a995 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -830,6 +830,35 @@ Proof.
     reflexivity.
 Qed.
 
+Lemma tm_step_repunit : forall (n : nat),
+  nth_error (tm_step n) (2^n - 1) = Some (odd n).
+Proof.
+  intros n.
+  rewrite nth_error_nth' with (d := false).
+  replace (tm_step n) with (rev (rev (tm_step n))).
+  rewrite rev_nth. rewrite rev_length.
+  rewrite tm_size_power2. rewrite <- Nat.sub_succ_l.
+  rewrite Nat.sub_succ. rewrite Nat.sub_0_r.
+  rewrite Nat.sub_diag. rewrite tm_step_end_1.
+  simpl. reflexivity.
+
+  rewrite Nat.le_succ_l. induction n. simpl. apply Nat.lt_0_1.
+  rewrite Nat.mul_lt_mono_pos_r with (p := 2) in IHn.
+  simpl in IHn. rewrite Nat.mul_comm in IHn.
+  rewrite <- Nat.pow_succ_r in IHn. apply IHn.
+  apply Nat.le_0_l. apply Nat.lt_0_2.
+
+  rewrite rev_length. rewrite tm_size_power2.
+  rewrite Nat.sub_1_r. apply Nat.lt_pred_l.
+  apply Nat.pow_nonzero. easy.
+
+  rewrite rev_involutive. reflexivity.
+  rewrite tm_size_power2.
+  rewrite Nat.sub_1_r. apply Nat.lt_pred_l.
+  apply Nat.pow_nonzero. easy.
+Qed.
+
+
 Lemma list_app_length_lt : forall (l l1 l2 : list bool) (b : bool),
   l = l1 ++ b :: l2 -> length l1 < length l.
 Proof.
@@ -1041,66 +1070,6 @@ Proof.
 Qed.
 
 
-Lemma tm_step_repunit : forall (n : nat),
-  nth_error (tm_step n) (2^n - 1) = Some (odd n).
-Proof.
-  intros n.
-  rewrite nth_error_nth' with (d := false).
-  replace (tm_step n) with (rev (rev (tm_step n))).
-  rewrite rev_nth. rewrite rev_length.
-  rewrite tm_size_power2. rewrite <- Nat.sub_succ_l.
-  rewrite Nat.sub_succ. rewrite Nat.sub_0_r.
-  rewrite Nat.sub_diag. rewrite tm_step_end_1.
-  simpl. reflexivity.
-
-  rewrite Nat.le_succ_l. induction n. simpl. apply Nat.lt_0_1.
-  rewrite Nat.mul_lt_mono_pos_r with (p := 2) in IHn.
-  simpl in IHn. rewrite Nat.mul_comm in IHn.
-  rewrite <- Nat.pow_succ_r in IHn. apply IHn.
-  apply Nat.le_0_l. apply Nat.lt_0_2.
-
-  rewrite rev_length. rewrite tm_size_power2.
-  rewrite Nat.sub_1_r. apply Nat.lt_pred_l.
-  apply Nat.pow_nonzero. easy.
-
-  rewrite rev_involutive. reflexivity.
-  rewrite tm_size_power2.
-  rewrite Nat.sub_1_r. apply Nat.lt_pred_l.
-  apply Nat.pow_nonzero. easy.
-Qed.
-
-  Nat.mul_lt_mono_neg_r: forall p n m : nat, p < 0 -> n < m <-> m * p < n * p
-
-
-  induction n. simpl. easy. simpl.
-
-
-Nat.le_succ_l: forall n m : nat, S n <= m <-> n < m
-  Nat.le_trans: forall n m p : nat, n <= m -> m <= p -> n <= p
-Nat.pow_nonzero: forall a b : nat, a <> 0 -> a ^ b <> 0
-
-
-rev_nth:
-  forall [A : Type] (l : list A) (d : A) [n : nat],
-  n < length l -> nth n (rev l) d = nth (length l - S n) l d
-
-nth_error_nth:
-  forall [A : Type] (l : list A) (n : nat) [x : A] (d : A),
-  nth_error l n = Some x -> nth n l d = x
-nth_error_nth':
-  forall [A : Type] (l : list A) [n : nat] (d : A),
-  n < length l -> nth_error l n = Some (nth n l d)
-
-Lemma tm_step_end_1 : forall (n : nat),
-  rev (tm_step n) = odd n :: tl (rev (tm_step n)).
-
-
-
-last_length:
-  forall [A : Type] (l : list A) (a : A),
-  length (l ++ a :: nil) = S (length l)
-
-
 
 
 Require Import BinPosDef.