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-04 16:13:58 +01:00
parent 44ae80ab27
commit 1e45967596
1 changed files with 5 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
thue_morse.v
View File

@ -375,12 +375,11 @@ Proof.
intro n.
rewrite <- Nat.sub_1_r. rewrite <- tm_size_power2.
rewrite nth_error_nth' with (d := false).
rewrite <- rev_nth. rewrite tm_step_end_1. simpl.
reflexivity.
rewrite tm_size_power2.
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
rewrite Nat.sub_1_r. apply Nat.lt_pred_l.
rewrite tm_size_power2. apply Nat.pow_nonzero. easy.
- rewrite <- rev_nth. rewrite tm_step_end_1. simpl. reflexivity.
rewrite tm_size_power2.
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
- rewrite Nat.sub_1_r. apply Nat.lt_pred_l.
rewrite tm_size_power2. apply Nat.pow_nonzero. easy.
Qed.