baruchel
/
coqbooks
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update

This commit is contained in:
Thomas Baruchel 2023-02-13 05:09:18 +01:00
parent a1e852daa3
commit 42ae58755d
1 changed files with 4 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/thue_morse4.v
View File

@ -1752,3 +1752,7 @@ Proof.
rewrite rev_length. rewrite firstn_length_le.
rewrite skipn_length. reflexivity. apply Nat.le_sub_l.
rewrite <- firstn_app. reflexivity.
rewrite app_length. rewrite Nat.pow_succ_r. rewrite I.
rewrite <- Nat.add_sub_assoc. rewrite <- Nat.mul_sub_distr_r.
apply Nat.le_add_r. apply Nat.mul_le_mono_r. lia. lia.
Qed.