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-03 13:57:21 +01:00
parent e5c270e119
commit eb8cccad44
1 changed files with 5 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
thue-morse.v
View File

@ -1302,9 +1302,10 @@ Proof.
rewrite M. apply tm_morphism_size.
assert (2 <= length (b++b++b++tl2)).
rewrite app_length. replace (2) with (2+0). apply Nat.add_le_mono. assumption.
apply Nat.le_0_l. apply Nat.add_0_r.
rewrite H3 in H4. replace (2) with (2*1) in H4. rewrite <- Nat.mul_le_mono_pos_l in H4.
rewrite app_length. rewrite <- Nat.add_0_r at 1.
apply Nat.add_le_mono. assumption. apply Nat.le_0_l.
rewrite H3 in H4. rewrite <- Nat.mul_1_r in H4 at 1.
rewrite <- Nat.mul_le_mono_pos_l in H4.
rewrite firstn_length. rewrite <- Nat.le_succ_l.
assert (1 <= Nat.div2 (length b)).
@ -1314,7 +1315,7 @@ Proof.
rewrite <- Nat.negb_even. rewrite J. simpl. rewrite Nat.add_0_r. reflexivity.
apply Nat.lt_0_2.
generalize H4. generalize H5. apply Nat.min_glb.
apply Nat.lt_0_2. easy.
apply Nat.lt_0_2.
Qed.