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-29 11:00:10 +01:00
parent 484e8d49b6
commit 4e3641242d
1 changed files with 2 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
thue-morse.v
View File

@ -735,11 +735,10 @@ Proof.
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.
rewrite <- Nat.mul_1_r 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.lt_0_succ. assumption. apply Nat.lt_0_2.
apply Nat.mul_comm. apply Nat.mul_comm.
Qed.