---

Step * 2 1 2 1 1 2 2 3 of Lemma div_unique3


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

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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index