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-26 07:54:12 +01:00
parent 5399610d21
commit a93c2a6607
1 changed files with 0 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
thue-morse.v
View File

@ -1102,7 +1102,6 @@ Proof.
generalize H1. generalize H0. apply Nat.lt_trans. rewrite <- H1.
rewrite tm_step_repunit_index. destruct (odd n). easy. easy.
rewrite Nat.succ_lt_mono. simpl.
(*
assert (K: nth_error (tm_step n) a = Some (odd n)). rewrite I.
apply tm_step_repunit.