baruchel/coqbooks
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update

Browse Source
This commit is contained in:
Thomas Baruchel 2022-11-22 22:50:46 +01:00
parent f922960785
commit 3195f3eb4e
1 changed files with 1 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
thue-morse.v
View File

@ -887,9 +887,7 @@ Proof.
assert (I: length l1 < 2^n).
rewrite <- tm_size_power2. generalize H. apply list_app_length_lt.
rewrite nth_error_app2. rewrite tm_size_power2.
replace (length l1 + 2^n - 2^n) with (length l1).
apply map_nth_error. apply H0.
rewrite Nat.add_sub. reflexivity.
rewrite Nat.add_sub. apply map_nth_error. apply H0.
rewrite tm_size_power2. apply Nat.le_add_l.
Qed.