Update
This commit is contained in:
parent
8604cc2d27
commit
0e43274f90
@ -662,10 +662,7 @@ Proof.
|
|||||||
rewrite <- Nat.mul_lt_mono_pos_l in I.
|
rewrite <- Nat.mul_lt_mono_pos_l in I.
|
||||||
assert (J := I). apply IHm in J.
|
assert (J := I). apply IHm in J.
|
||||||
|
|
||||||
assert (M: 0 < 2^m). destruct m. simpl. apply Nat.lt_0_1.
|
assert (M: 0 < 2^m). rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
|
||||||
replace (0) with (0 ^ (S m)) at 1.
|
|
||||||
apply Nat.pow_lt_mono_l. apply Nat.neq_succ_0. apply Nat.lt_0_2.
|
|
||||||
apply Nat.pow_0_l. apply Nat.neq_succ_0.
|
|
||||||
|
|
||||||
assert (L: S (2 * k) * 2 ^ m - 1 < S (2 * k) * 2 ^ m).
|
assert (L: S (2 * k) * 2 ^ m - 1 < S (2 * k) * 2 ^ m).
|
||||||
replace (S (2 * k) * 2 ^ m) with (S (S (2 * k) * 2 ^ m - 1)) at 2.
|
replace (S (2 * k) * 2 ^ m) with (S (S (2 * k) * 2 ^ m - 1)) at 2.
|
||||||
|
Loading…
Reference in New Issue
Block a user