Update
This commit is contained in:
parent
3b91125216
commit
5399610d21
@ -1100,7 +1100,7 @@ Proof.
|
|||||||
assert (2^n < 2^(S n)). apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
|
assert (2^n < 2^(S n)). apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
|
||||||
apply Nat.lt_succ_diag_r.
|
apply Nat.lt_succ_diag_r.
|
||||||
generalize H1. generalize H0. apply Nat.lt_trans. rewrite <- H1.
|
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.
|
rewrite Nat.succ_lt_mono. simpl.
|
||||||
(*
|
(*
|
||||||
|
Loading…
Reference in New Issue
Block a user