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-14 20:31:22 +01:00
parent e1238e5198
commit db1b42ac8c
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/thue_morse.v
View File

@ -413,7 +413,7 @@ Proof.
apply tm_step_count_occ.
rewrite count_occ_app in L. rewrite count_occ_app in L.
rewrite K in L. rewrite Nat.add_cancel_l in L.
destruct b. simpl in L. inversion L. simpl in L. inversion L.
destruct b; simpl in L; inversion L.
Qed.
Lemma tm_step_consecutive_identical' :