Update
This commit is contained in:
parent
1ae999e04a
commit
b830335fea
10
thue-morse.v
10
thue-morse.v
|
@ -869,15 +869,13 @@ Proof.
|
||||||
rewrite H1. easy.
|
rewrite H1. easy.
|
||||||
rewrite nth_error_Some in I. rewrite tm_size_power2 in I.
|
rewrite nth_error_Some in I. rewrite tm_size_power2 in I.
|
||||||
assert (2^k <= length l1 + 2^k).
|
assert (2^k <= length l1 + 2^k).
|
||||||
apply Nat.le_add_l.
|
apply Nat.le_add_l. generalize I. generalize H3. apply Nat.le_lt_trans.
|
||||||
generalize I. generalize H3.
|
|
||||||
apply Nat.le_lt_trans.
|
|
||||||
}
|
}
|
||||||
|
|
||||||
assert (k < n). {
|
assert (k < n). { generalize H3. apply Nat.pow_lt_mono_r_iff.
|
||||||
generalize H3. apply Nat.pow_lt_mono_r_iff.
|
apply Nat.lt_succ_diag_r. }
|
||||||
|
|
||||||
|
|
||||||
BEFORE REPLACEMENT.
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue
Block a user