---

Step * of Lemma le-iff-less-or-equal

∀x,y:ℤ.  uiff(x ≤ y;x < y ∨ (x = y ∈ ℤ))
BY
{ TACTIC:Auto }

1
1. x : ℤ
2. y : ℤ
3. x ≤ y
⊢ x < y ∨ (x = y ∈ ℤ)

2
1. x : ℤ
2. y : ℤ
3. x < y ∨ (x = y ∈ ℤ)
⊢ x ≤ y

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbZ{}.    uiff(x  \mleq{}  y;x  <  y  \mvee{}  (x  =  y))


By

---

Latex:
TACTIC:Auto

---

Home Index