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-23 09:15:58 +01:00
parent 4b36fa4531
commit e0754cb433
1 changed files with 2 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
thue-morse.v
View File

@ -867,10 +867,8 @@ Proof.
intros n l1 l2 b. intros H.
assert (nth_error (tm_step n) (length l1) = Some b).
generalize H. apply list_concat_to_pos.
rewrite tm_build.
assert (length l1 < length (tm_step n)).
generalize H. apply list_app_length_lt.
rewrite nth_error_app1. apply H0. apply H1.
rewrite tm_build. rewrite nth_error_app1. apply H0.
generalize H. apply list_app_length_lt.
Qed.
Lemma tm_step_next_range' :