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-12-13 13:50:33 +01:00
parent 27cdbf88b2
commit f6d6f3f693
1 changed files with 5 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
thue-morse.v
View File

@ -1231,6 +1231,7 @@ Proof.
assert (O: k*2^m + 2^j < 2^n). assert (O: k*2^m + 2^j < 2^n).
apply lt_split_bits. assumption. assumption. assumption. apply lt_split_bits. assumption. assumption. assumption.
assert (P: 2^n <= 2^(m+n)). apply Nat.pow_le_mono_r. easy. apply Nat.le_add_l.
assert ( nth_error (tm_step m) 0 assert ( nth_error (tm_step m) 0
= nth_error (tm_step m) (2^j) = nth_error (tm_step m) (2^j)
@ -1265,14 +1266,12 @@ Proof.
apply H1 in H2. rewrite H2 at 1. easy. easy. apply H1 in H2. rewrite H2 at 1. easy. easy.
rewrite nth_error_nth' with (d := false). easy. rewrite nth_error_nth' with (d := false). easy.
rewrite tm_size_power2. assumption. rewrite tm_size_power2. assumption.
apply tm_step_stable. assumption.
assert (2^n <= 2^(m+n)). apply Nat.pow_le_mono_r. easy. apply Nat.le_add_l.
generalize H1. generalize O. apply Nat.lt_le_trans.
apply tm_step_stable. assumption. apply tm_step_stable. assumption.
assert (2^n <= 2^(m+n)). apply Nat.pow_le_mono_r. easy. apply Nat.le_add_l. generalize P. generalize O. apply Nat.lt_le_trans.
generalize H1. generalize I. apply Nat.lt_le_trans.
apply tm_step_stable. assumption.
generalize P. generalize I. apply Nat.lt_le_trans.
Qed. Qed.