Compare commits
2 Commits
3b91125216
...
a93c2a6607
Author | SHA1 | Date | |
---|---|---|---|
|
a93c2a6607 | ||
|
5399610d21 |
@ -1100,9 +1100,8 @@ Proof.
|
||||
assert (2^n < 2^(S n)). apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
|
||||
apply Nat.lt_succ_diag_r.
|
||||
generalize H1. generalize H0. apply Nat.lt_trans. rewrite <- H1.
|
||||
rewrite tm_step_repunit_index.
|
||||
rewrite tm_step_repunit_index. destruct (odd n). easy. easy.
|
||||
|
||||
rewrite Nat.succ_lt_mono. simpl.
|
||||
(*
|
||||
assert (K: nth_error (tm_step n) a = Some (odd n)). rewrite I.
|
||||
apply tm_step_repunit.
|
||||
|
Loading…
Reference in New Issue
Block a user