---

Step * of Lemma le_transitivity

∀[x,y,z:ℤ].  (x ≤ z) supposing ((y ≤ z) and (x ≤ y))
BY
{ TACTIC:((UnivCD THENA Auto)
          THEN (All (RWO "le-iff-nonneg")⋅ THENA Auto)
          THEN (FLemma `add-nonneg` [-1;-2]⋅ THENA Auto)) }

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

---

Latex:

---

Latex:
\mforall{}[x,y,z:\mBbbZ{}].    (x  \mleq{}  z)  supposing  ((y  \mleq{}  z)  and  (x  \mleq{}  y))


By

---

Latex:
TACTIC:((UnivCD  THENA  Auto)
                THEN  (All  (RWO  "le-iff-nonneg")\mcdot{}  THENA  Auto)
                THEN  (FLemma  `add-nonneg`  [-1;-2]\mcdot{}  THENA  Auto))

---

Home Index