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-26 23:34:57 +01:00
parent 30a2634ace
commit a1186e0654
1 changed files with 12 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
src/thue_morse3.v
View File

@ -1591,6 +1591,18 @@ Proof.
rewrite Nat.pow_succ_r. rewrite Nat.even_mul. reflexivity.
apply Nat.le_0_l.
assert (J': even (length a') = true). unfold a'. rewrite firstn_length.
rewrite skipn_length.
assert (C: Nat.div2 (length a) <= length (tm_step n) - Nat.div2 (length hd)
\/ length (tm_step n) - Nat.div2 (length hd) < Nat.div2 (length a)).
apply Nat.le_gt_cases. destruct C.
apply Nat.min_r in H6. rewrite Nat.min_comm. rewrite H6. apply EVEN2.
assumption. apply Nat.lt_le_incl in H6.
apply Nat.min_l in H6. rewrite Nat.min_comm. rewrite H6.
rewrite tm_size_power2. destruct n. inversion V. inversion H8.
rewrite Nat.pow_succ_r. rewrite Nat.even_sub. rewrite Nat.even_mul.
assert (Nat.even (Nat.div2 (length hd)) = true). apply EVEN2. assumption.
rewrite H7. reflexivity.