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 2022-11-25 11:47:07 +01:00
parent afc7173251
commit a3f15b3984
1 changed files with 4 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
thue-morse.v
View File

@ -1110,7 +1110,10 @@ Lemma tm_step_next_range2_neighbor' : forall (n k : nat),
rewrite <- H2. rewrite <- H3. apply L. rewrite <- H2. rewrite <- H3. apply L.
apply H0. apply H0.
- - induction m.
+ intros L. rewrite Nat.add_0_r in L. rewrite Nat.add_0_r in L.
apply tm_step_next_range2_neighbor'. apply H. apply L.
+