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 2022-12-28 19:27:22 +01:00
parent b51cd1781a
commit ba491a33d3
1 changed files with 0 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
thue-morse.v
View File

@ -627,12 +627,6 @@ Proof.
Qed. Qed.
Lemma tm_step_pred : forall (n k m : nat), Lemma tm_step_pred : forall (n k m : nat),
S (2*k) * 2^m < 2^n -> ( S (2*k) * 2^m < 2^n -> (
nth_error (tm_step n) (S (2*k) * 2^m) nth_error (tm_step n) (S (2*k) * 2^m)
@ -660,7 +654,6 @@ Proof.
replace (S (2*k) * 2) with (2* (S (2*k))). replace (S (2*k) * 2) with (2* (S (2*k))).
rewrite <- Nat.mul_assoc. rewrite <- tm_step_double_index. rewrite <- Nat.mul_assoc. rewrite <- tm_step_double_index.
(* réécriture de I *)
rewrite Nat.pow_succ_r' in I. rewrite Nat.pow_succ_r' in I.
rewrite Nat.pow_succ_r' in I. rewrite Nat.pow_succ_r' in I.
rewrite Nat.mul_assoc in I. rewrite Nat.mul_assoc in I.