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:26:04 +01:00
parent 7c7bc16120
commit 656fb217b1
1 changed files with 26 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
thue-morse.v
View File

@ -746,8 +746,34 @@ Proof.
apply Nat.lt_trans.
rewrite tm_size_power2. assumption.
rewrite Nat.mul_sub_distr_l. rewrite Nat.mul_1_r.
rewrite <- Nat.sub_succ_l.
rewrite Nat.sub_succ. reflexivity.
replace (2) with (2*1) at 1.
apply Nat.mul_le_mono_pos_l. apply Nat.lt_0_2.
apply Nat.le_succ_l. apply Nat.mul_pos_pos.
apply Nat.lt_0_succ. assumption. apply Nat.mul_1_r.
apply Nat.lt_0_2.
apply Nat.mul_comm.
apply Nat.mul_comm.
Qed.
replace (S (2 * (S (2 * k) * 2 ^ m))) with (2 * (S (2 * k) * 2 ^ m) + 1).
rewrite <- Nat.add_cancel_r with (p := 1).
rewrite Nat.sub_add. rewrite <- Nat.add_sub_assoc. rewrite Nat.add_shuffle0.
rewrite <- Nat.add_assoc.
rewrite Nat.sub_succ.
rewrite <- Nat.add_cancel_r with (p := 1).
rewrite Nat.sub_add. rewrite <- Nat.add_assoc.
rewrite
replace (S (2 * (S (2 * k) * 2 ^ m))) with (2 * (S (2 * k) * 2 ^ m) + 1).
rewrite <- Nat.add_cancel_r with (p := 1).
rewrite Nat.sub_add.