Update
This commit is contained in:
parent
e4e0052d90
commit
6c015eff1d
@ -1209,11 +1209,9 @@ Proof.
|
|||||||
assert (N: nth_error (tm_step m) (2^j) = Some true).
|
assert (N: nth_error (tm_step m) (2^j) = Some true).
|
||||||
replace (nth_error (tm_step m) (2^j)) with (nth_error (tm_step (S j)) (2^j)).
|
replace (nth_error (tm_step m) (2^j)) with (nth_error (tm_step (S j)) (2^j)).
|
||||||
rewrite tm_step_single_bit_index. reflexivity.
|
rewrite tm_step_single_bit_index. reflexivity.
|
||||||
apply tm_step_stable. rewrite <- Nat.mul_1_l at 1.
|
apply tm_step_stable.
|
||||||
rewrite Nat.pow_succ_r. rewrite <- Nat.mul_lt_mono_pos_r.
|
apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. apply Nat.lt_succ_diag_r.
|
||||||
apply Nat.lt_1_2.
|
assumption.
|
||||||
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
|
|
||||||
apply Nat.le_0_l. assumption.
|
|
||||||
|
|
||||||
assert (G: k = 0 \/ 0 < k). apply Nat.eq_0_gt_0_cases. destruct G.
|
assert (G: k = 0 \/ 0 < k). apply Nat.eq_0_gt_0_cases. destruct G.
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user