---

Step * 2 of Lemma less-iff-positive


1. x : ℤ
2. y : ℤ
3. 0 < y - x
⊢ x < y
BY
{ TACTIC:(Assert 0 + x < (y - x) + x BY
                (BLemma `add-monotonic` THEN Auto)) }

1
1. x : ℤ
2. y : ℤ
3. 0 < y - x
4. 0 + x < (y - x) + x
⊢ x < y

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}
2.  y  :  \mBbbZ{}
3.  0  <  y  -  x
\mvdash{}  x  <  y


By

---

Latex:
TACTIC:(Assert  0  +  x  <  (y  -  x)  +  x  BY
                            (BLemma  `add-monotonic`  THEN  Auto))

---

Home Index