---

Step * of Lemma less_than_transitivity1

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

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  \mleq{}  z)  and  x  <  y)


By

---

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

---

Home Index