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 2023-01-06 17:17:20 +01:00
parent 94c0e535ef
commit d3bc94288a
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/thue_morse.v
View File

@ -782,12 +782,12 @@ Theorem tm_step_succ_double_index : forall (n k : nat),
k < 2^n -> nth_error (tm_step n) k <> nth_error (tm_step (S n)) (S (2*k)).
Proof.
intros n k. intro H. rewrite tm_step_double_index.
rewrite Nat.mul_comm. replace (2) with (2^1).
rewrite Nat.mul_comm. rewrite <- Nat.pow_1_r with (a := 2).
replace (S (k*2^1)) with (k*2^1 + 2^0).
apply tm_step_flip_low_bit. apply Nat.lt_0_1.
rewrite Nat.mul_comm. simpl. rewrite Nat.add_0_r. rewrite Nat.add_0_r.
apply Nat.add_lt_mono; assumption.
simpl. rewrite Nat.add_1_r. reflexivity. apply Nat.pow_1_r.
simpl. apply Nat.add_1_r.
Qed.