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:42:58 +01:00
parent 0fe7e6dd25
commit 1aea07ca1f
1 changed files with 4 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
src/thue_morse3.v
View File

@ -966,7 +966,10 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
apply Nat.lt_0_succ. apply Nat.le_refl. apply Nat.lt_0_succ. apply Nat.le_refl.
apply Nat.lt_le_incl. assumption. reflexivity. reflexivity. apply Nat.lt_le_incl. assumption. reflexivity. reflexivity.
assumption. apply Nat.lt_0_succ. assumption. apply Nat.lt_0_succ.
apply Nat.div_le_mono with (c := 8) in T. rewrite Nat.div_same in T.
rewrite Nat.le_succ_l in T. assumption. easy. easy.
(* on change de modulo ; on travaille sur 8k+6 maintenant *)