---

Step * 2 1 2 1 1 2 2 4 of Lemma div_unique3


1. x : ℤ
2. ¬0 < x
3. y : ℤ
4. ¬0 < x - y
5. ¬0 < y
6. z : ℤ
7. 0 < x ⇒ (0 ≤ y)
8. 0 < y ⇒ (0 ≤ x)
9. ¬(x = 0 ∈ ℤ)
10. ¬(y = 0 ∈ ℤ)
11. -x < z
12. -y < z
⊢ -(x - y) < z
BY
{ TACTIC:(Assert ⌜(-(x - y)) ≤ (-x)⌝⋅ THEN Auto) }

1
.....assertion..... 
1. x : ℤ
2. ¬0 < x
3. y : ℤ
4. ¬0 < x - y
5. ¬0 < y
6. z : ℤ
7. 0 < x ⇒ (0 ≤ y)
8. 0 < y ⇒ (0 ≤ x)
9. ¬(x = 0 ∈ ℤ)
10. ¬(y = 0 ∈ ℤ)
11. -x < z
12. -y < z
⊢ (-(x - y)) ≤ (-x)

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}
2.  \mneg{}0  <  x
3.  y  :  \mBbbZ{}
4.  \mneg{}0  <  x  -  y
5.  \mneg{}0  <  y
6.  z  :  \mBbbZ{}
7.  0  <  x  {}\mRightarrow{}  (0  \mleq{}  y)
8.  0  <  y  {}\mRightarrow{}  (0  \mleq{}  x)
9.  \mneg{}(x  =  0)
10.  \mneg{}(y  =  0)
11.  -x  <  z
12.  -y  <  z
\mvdash{}  -(x  -  y)  <  z


By

---

Latex:
TACTIC:(Assert  \mkleeneopen{}(-(x  -  y))  \mleq{}  (-x)\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index