---

Step * of Lemma le-add-shift

∀[x,y,z:ℤ].  uiff(x ≤ (y + z);((-y) + x) ≤ z)
BY
{ ((UnivCD THENA Auto) THEN (RepeatFor 2 (D 0) THENA Auto)) }

1
1. x : ℤ
2. y : ℤ
3. z : ℤ
4. x ≤ (y + z)
⊢ ((-y) + x) ≤ z

2
1. x : ℤ
2. y : ℤ
3. z : ℤ
4. ((-y) + x) ≤ z
⊢ x ≤ (y + z)

---

Latex:

---

Latex:
\mforall{}[x,y,z:\mBbbZ{}].    uiff(x  \mleq{}  (y  +  z);((-y)  +  x)  \mleq{}  z)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (RepeatFor  2  (D  0)  THENA  Auto))

---

Home Index