Update
This commit is contained in:
parent
ea8e07d20d
commit
484e8d49b6
@ -686,9 +686,7 @@ Proof.
|
|||||||
|
|
||||||
assert (nth_error (tm_step n0) ((S (2 * k) * 2 ^ m) - 1)
|
assert (nth_error (tm_step n0) ((S (2 * k) * 2 ^ m) - 1)
|
||||||
<> nth_error (tm_step (S n0)) (S (2 * (S (2 * k) * 2 ^ m - 1)))).
|
<> nth_error (tm_step (S n0)) (S (2 * (S (2 * k) * 2 ^ m - 1)))).
|
||||||
apply tm_step_succ_double_index.
|
apply tm_step_succ_double_index. assumption.
|
||||||
|
|
||||||
assumption.
|
|
||||||
|
|
||||||
replace (S (2 * (S (2 * k) * 2 ^ m - 1))) with (2 * (S (2*k) * 2^m) - 1) in H.
|
replace (S (2 * (S (2 * k) * 2 ^ m - 1))) with (2 * (S (2*k) * 2^m) - 1) in H.
|
||||||
rewrite Nat.odd_succ. rewrite <- Nat.negb_odd. destruct (odd m).
|
rewrite Nat.odd_succ. rewrite <- Nat.negb_odd. destruct (odd m).
|
||||||
|
Loading…
Reference in New Issue
Block a user