Update
This commit is contained in:
parent
7fc74784db
commit
7c36b66a21
17
thue-morse.v
17
thue-morse.v
@ -946,20 +946,15 @@ Proof.
|
||||
intros n k. intros H.
|
||||
rewrite tm_build.
|
||||
rewrite nth_error_app2. rewrite tm_size_power2. rewrite Nat.add_sub.
|
||||
|
||||
assert (nth_error (tm_step n) k = Some (nth k (tm_step n) false)).
|
||||
generalize H. rewrite <- tm_size_power2. apply nth_error_nth'.
|
||||
rewrite H0.
|
||||
|
||||
assert (nth_error (map negb (tm_step n)) k =
|
||||
Some (negb (nth k (tm_step n) false))).
|
||||
generalize H0. apply map_nth_error.
|
||||
rewrite H1.
|
||||
|
||||
|
||||
destruct (nth_error (tm_step n) k). rewrite <- H0. rewrite <- H0.
|
||||
|
||||
|
||||
assert (nth_error (map negb (tm_step n)) k
|
||||
= Some (negb (nth k (tm_step n) false))).
|
||||
generalize H0. apply map_nth_error. rewrite H1.
|
||||
destruct (nth k (tm_step n) false). easy. easy.
|
||||
rewrite tm_size_power2. apply Nat.le_add_l.
|
||||
Qed.
|
||||
|
||||
|
||||
|
||||
|
Loading…
x
Reference in New Issue
Block a user