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 14:56:21 +01:00
parent d938efe215
commit 2489ad0497
1 changed files with 1 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
thue-morse.v
View File

@ -1338,7 +1338,7 @@ Qed.
Lemma tm_step_add_small_power : Lemma tm_step_flip_low_bit :
forall (n m k j : nat), forall (n m k j : nat),
0 < k -> j < m -> k * 2^m < 2^n 0 < k -> j < m -> k * 2^m < 2^n
-> nth_error (tm_step n) (k * 2^m) <> nth_error (tm_step n) (k * 2^m + 2^j). -> nth_error (tm_step n) (k * 2^m) <> nth_error (tm_step n) (k * 2^m + 2^j).
@ -1407,21 +1407,6 @@ Qed.
Lemma greedy_power2 : forall (n m : nat),
0 < n -> n = 2^(Nat.log2 n) + m -> m < 2^(Nat.log2 n).
Proof.
intros n m. intros H I.
rewrite Nat.add_lt_mono_l with (p := 2^(Nat.log2 n)).
rewrite <- I.
replace (2^(Nat.log2 n) + 2^(Nat.log2 n)) with (2* (2^(Nat.log2 n))).
rewrite <- Nat.pow_succ_r.
apply Nat.log2_spec. apply H. apply Nat.log2_nonneg.
simpl. rewrite Nat.add_0_r. reflexivity.
Qed.