---

Step * 2 1 1 2 1 1 of Lemma decidable__proper_divisor


1. v : ℕ
⊢ (v^4 ≤ (((v + 1) * (v + 1)) + 1)) ⇒ v < 2
BY
{ TACTIC:Assert ⌜(2 ≤ v) ⇒ ((v + 1) * (v + 1)) + 1 < v^4⌝⋅ }

1
.....assertion..... 
1. v : ℕ
⊢ (2 ≤ v) ⇒ ((v + 1) * (v + 1)) + 1 < v^4

2
1. v : ℕ
2. (2 ≤ v) ⇒ ((v + 1) * (v + 1)) + 1 < v^4
⊢ (v^4 ≤ (((v + 1) * (v + 1)) + 1)) ⇒ v < 2

---

Latex:

---

Latex:

1.  v  :  \mBbbN{}
\mvdash{}  (v\^{}4  \mleq{}  (((v  +  1)  *  (v  +  1))  +  1))  {}\mRightarrow{}  v  <  2


By

---

Latex:
TACTIC:Assert  \mkleeneopen{}(2  \mleq{}  v)  {}\mRightarrow{}  ((v  +  1)  *  (v  +  1))  +  1  <  v\^{}4\mkleeneclose{}\mcdot{}

---

Home Index