---

Step * 1 2 1 of Lemma nat-retractible


1. x : Base
2. (if (x) < (0)  then ⊥  else x)↓
3. x ∈ ℤ
4. 0 ∈ ℤ
⊢ x ∈ ℕ
BY
{ TACTIC:(MoveToConcl (-3) THEN AutoSplit THEN Auto THEN BotDiv) }

---

Latex:

---

Latex:

1.  x  :  Base
2.  (if  (x)  <  (0)    then  \mbot{}    else  x)\mdownarrow{}
3.  x  \mmember{}  \mBbbZ{}
4.  0  \mmember{}  \mBbbZ{}
\mvdash{}  x  \mmember{}  \mBbbN{}


By

---

Latex:
TACTIC:(MoveToConcl  (-3)  THEN  AutoSplit  THEN  Auto  THEN  BotDiv)

---

Home Index