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 14:25:35 +01:00
parent a85580d0e5
commit 94c0e535ef
1 changed files with 2 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
src/thue_morse.v
View File

@ -785,10 +785,9 @@ Proof.
rewrite Nat.mul_comm. replace (2) with (2^1).
replace (S (k*2^1)) with (k*2^1 + 2^0).
apply tm_step_flip_low_bit. apply Nat.lt_0_1.
simpl. rewrite Nat.add_0_r. replace (k*2) with (k+k).
rewrite Nat.mul_comm. simpl. rewrite Nat.add_0_r. rewrite Nat.add_0_r.
apply Nat.add_lt_mono; assumption.
rewrite Nat.mul_comm. simpl. rewrite Nat.add_0_r. reflexivity.
simpl. rewrite Nat.add_1_r. reflexivity. reflexivity.
simpl. rewrite Nat.add_1_r. reflexivity. apply Nat.pow_1_r.
Qed.