Update
This commit is contained in:
parent
f6d6f3f693
commit
065a7df946
@ -1229,8 +1229,7 @@ Proof.
|
||||
(* k < 0 *)
|
||||
rename H0 into G.
|
||||
|
||||
assert (O: k*2^m + 2^j < 2^n).
|
||||
apply lt_split_bits. assumption. assumption. assumption.
|
||||
assert (O: k*2^m + 2^j < 2^n). apply lt_split_bits; assumption.
|
||||
assert (P: 2^n <= 2^(m+n)). apply Nat.pow_le_mono_r. easy. apply Nat.le_add_l.
|
||||
|
||||
assert ( nth_error (tm_step m) 0
|
||||
|
Loading…
Reference in New Issue
Block a user