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

Update

This commit is contained in:
Thomas Baruchel 2023-01-22 21:48:19 +01:00
parent a12c0e3fd2
commit fde534fcc0
1 changed files with 6 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/thue_morse3.v
View File

@ -943,7 +943,13 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
rewrite <- Nat.add_le_mono_r. destruct hd. inversion Q.
simpl. apply le_n_S. apply le_0_n. reflexivity. reflexivity.
apply Nat.lt_le_incl. assumption.
rewrite <- tm_step_repeating_patterns in H10. inversion H10.
simpl. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
simpl. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
unfold lh.