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-10 22:21:07 +01:00
parent d27fdab010
commit de7cc14376
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
thue-morse.v
View File

@ -1265,10 +1265,10 @@ Proof.
assumption. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption. assumption. assumption. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption. assumption.
apply tm_step_stable. apply lt_split_bits. apply tm_step_stable. apply lt_split_bits.
assumption. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption. assumption. assumption. assumption. assumption.
assert (k*2^m + 2^j < 2^n). assert (k*2^m + 2^j < 2^n).
apply lt_split_bits. apply lt_split_bits.
assumption. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption. assumption. assumption. assumption. assumption.
assert (2^n <= 2^(m+n)). apply Nat.pow_le_mono_r. easy. apply Nat.le_add_l. assert (2^n <= 2^(m+n)). apply Nat.pow_le_mono_r. easy. apply Nat.le_add_l.
generalize H2. generalize H1. apply Nat.lt_le_trans. generalize H2. generalize H1. apply Nat.lt_le_trans.