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

Compare commits

base: baruchel:a93c2a6607080e6fde066ce33958a48167f2c5be
Branches Tags
baruchel:master
..
compare: baruchel:3b91125216fbccff920469bc01a96570d6bdb2b8
Branches Tags
baruchel:master

No commits in common. "a93c2a6607080e6fde066ce33958a48167f2c5be" and "3b91125216fbccff920469bc01a96570d6bdb2b8" have entirely different histories.
a93c2a6607 ... 3b91125216

1 changed files with 2 additions and 1 deletions
Show Stats Expand all files Collapse all files

3
thue-morse.v
View File

@ -1100,8 +1100,9 @@ Proof.
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. destruct (odd n). easy. easy.
rewrite tm_step_repunit_index.
rewrite Nat.succ_lt_mono. simpl.
(*
assert (K: nth_error (tm_step n) a = Some (odd n)). rewrite I.
apply tm_step_repunit.