---

Step * of Lemma less_than_transitivity2

∀[x,y,z:ℤ].  (x < z) supposing (y < z and (x ≤ y))
BY
{ (TACTIC:Auto THEN (RWO "le-iff-less-or-equal" (-2) THENA Auto) THEN D -2) }

1
1. x : ℤ
2. y : ℤ
3. z : ℤ
4. x < y
5. y < z
⊢ x < z

2
1. x : ℤ
2. y : ℤ
3. z : ℤ
4. x = y ∈ ℤ
5. y < z
⊢ x < z

---

Latex:

---

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


By

---

Latex:
(TACTIC:Auto  THEN  (RWO  "le-iff-less-or-equal"  (-2)  THENA  Auto)  THEN  D  -2)

---

Home Index