Update
This commit is contained in:
parent
0cf8e80ecf
commit
3b91125216
12
thue-morse.v
12
thue-morse.v
@ -1091,12 +1091,16 @@ Proof.
|
||||
intros k b n m. intros H I.
|
||||
assert (J: nth_error (tm_step (S n)) (2^n-1) = nth_error (tm_step (S n)) (2^n)
|
||||
<-> odd n = true).
|
||||
rewrite tm_step_single_bit_index.
|
||||
assert (nth_error (tm_step n) (2^n - 1) = nth_error (tm_step (S n)) (2^n-1)).
|
||||
apply tm_step_stable.
|
||||
assert (2^n - 1 < 2^n).
|
||||
apply Nat.sub_lt. replace (1) with (2^0) at 1. apply Nat.pow_le_mono_r.
|
||||
easy. apply le_0_n. simpl. reflexivity. apply Nat.lt_0_1. apply H0.
|
||||
easy. apply le_0_n. simpl. reflexivity. apply Nat.lt_0_1.
|
||||
rewrite tm_step_single_bit_index.
|
||||
assert (nth_error (tm_step n) (2^n - 1) = nth_error (tm_step (S n)) (2^n-1)).
|
||||
apply tm_step_stable. apply H0.
|
||||
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 Nat.succ_lt_mono. simpl.
|
||||
(*
|
||||
|
Loading…
Reference in New Issue
Block a user