---

Step * of Lemma less-trichotomy

∀a,b:ℤ.  (a < b ∨ b < a ∨ (a = b ∈ ℤ))
BY
{ (Auto THEN UseLessCases ⌜a⌝ ⌜b⌝⋅ THEN Auto) }

1
1. a : ℤ
2. b : ℤ
3. x : ∀[u,v:Base].  (if (a) < (b)  then u  else v ~ u)
⊢ a < b ∨ b < a ∨ (a = b ∈ ℤ)

2
1. a : ℤ
2. b : ℤ
3. x : ∀[u,v:Base].  (if (a) < (b)  then u  else v ~ v)
⊢ a < b ∨ b < a ∨ (a = b ∈ ℤ)

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbZ{}.    (a  <  b  \mvee{}  b  <  a  \mvee{}  (a  =  b))


By

---

Latex:
(Auto  THEN  UseLessCases  \mkleeneopen{}a\mkleeneclose{}  \mkleeneopen{}b\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index