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-22 22:28:24 +01:00
parent fde534fcc0
commit 358404d2be
1 changed files with 8 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
src/thue_morse3.v
View File

@ -949,8 +949,14 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
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.
rewrite Nat.mul_lt_mono_pos_l with (p := 8).
rewrite Nat.add_lt_mono_r with (p := 2). rewrite <- H9.
rewrite Nat.add_lt_mono_r with (p := 8).
rewrite <- Nat.add_sub_swap. rewrite Nat.add_sub.
rewrite <- Nat.add_assoc. replace (2+8) with 10.
replace (8) with (2^3) at 1. rewrite <- Nat.pow_add_r.
rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap. simpl.