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:36:25 +01:00
parent a304f0a9a8
commit a12c0e3fd2
1 changed files with 17 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
src/thue_morse3.v
View File

@ -921,7 +921,7 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
rewrite <- Nat.add_succ_comm. rewrite <- Nat.add_succ_comm.
rewrite <- Nat.add_succ_comm. rewrite app_length in T.
assumption. reflexivity. rewrite Y''.
rewrite app_length.
rewrite app_length.
replace (length (b3::b5::b7::hd)) with (S (S (S (length hd)))).
rewrite Nat.add_succ_comm. rewrite Nat.add_succ_comm.
rewrite Nat.add_succ_comm. rewrite <- Nat.sub_succ_l.
@ -930,7 +930,22 @@ rewrite app_length.
rewrite Nat.add_succ_r. rewrite Nat.add_succ_r.
rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono.
rewrite <- Nat.succ_le_mono. replace 5 with (1 + 4).
rewrite <- Nat.add_le_mono_r.
rewrite <- Nat.add_le_mono_r. destruct hd. inversion Q.
simpl. apply le_n_S. apply le_0_n. reflexivity. reflexivity.
rewrite Y''. rewrite app_length.
replace (length (b3::b5::b7::hd)) with (S (S (S (length hd)))).
rewrite Nat.add_succ_comm. rewrite Nat.add_succ_comm.
rewrite Nat.add_succ_comm. rewrite <- Nat.sub_succ_l.
rewrite <- Nat.add_succ_r. rewrite Nat.add_sub. apply Nat.le_refl.
rewrite Nat.add_succ_r. rewrite Nat.add_succ_r. rewrite Nat.add_succ_r.
rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono.
rewrite <- Nat.succ_le_mono. replace 5 with (1 + 4).
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.