Update
This commit is contained in:
parent
e885bb3a7e
commit
0cf8e80ecf
|
@ -1096,7 +1096,7 @@ Proof.
|
||||||
apply tm_step_stable.
|
apply tm_step_stable.
|
||||||
assert (2^n - 1 < 2^n).
|
assert (2^n - 1 < 2^n).
|
||||||
apply Nat.sub_lt. replace (1) with (2^0) at 1. apply Nat.pow_le_mono_r.
|
apply Nat.sub_lt. replace (1) with (2^0) at 1. apply Nat.pow_le_mono_r.
|
||||||
easy. apply le_0_n. simpl. reflexivity. apply Nat.lt_0_1.
|
easy. apply le_0_n. simpl. reflexivity. apply Nat.lt_0_1. apply H0.
|
||||||
|
|
||||||
rewrite Nat.succ_lt_mono. simpl.
|
rewrite Nat.succ_lt_mono. simpl.
|
||||||
(*
|
(*
|
||||||
|
|
Loading…
Reference in New Issue
Block a user