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-04 15:29:11 +01:00
parent dcfa1b363c
commit dce599bcb3
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
thue-morse.v
View File

@ -637,9 +637,9 @@ Proof.
rewrite H2. apply IHn.
rewrite Nat.add_lt_mono_r with (p := 2^n). rewrite Nat.sub_add.
rewrite Nat.pow_succ_r in H0. replace (2) with (1+1) in H0.
rewrite Nat.pow_succ_r in H0. rewrite <- Nat.add_1_r in H0 at 1.
rewrite Nat.mul_add_distr_r in H0. simpl in H0.
rewrite Nat.add_0_r in H0. assumption. reflexivity.
rewrite Nat.add_0_r in H0. assumption.
apply Nat.le_0_l. assumption.
rewrite Nat.mul_sub_distr_r. rewrite <- Nat.pow_add_r.