---

Step * 2 1 of Lemma less-iff-positive


1. x : ℤ
2. y : ℤ
3. 0 < y - x
4. 0 + x < (y - x) + x
⊢ x < y
BY
{ TACTIC:((RW (SubC IntNormC) (-1) THENM Hypothesis) THENA Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}
2.  y  :  \mBbbZ{}
3.  0  <  y  -  x
4.  0  +  x  <  (y  -  x)  +  x
\mvdash{}  x  <  y


By

---

Latex:
TACTIC:((RW  (SubC  IntNormC)  (-1)  THENM  Hypothesis)  THENA  Auto)

---

Home Index