---

Step * 1 of Lemma qle-iff


1. a : ℚ@i
2. b : ℚ@i
3. a < b ∨ (a = b ∈ ℚ) ∨ b < a
4. uiff(¬a < b;b ≤ a)
⊢ uiff(a ≤ b;a < b ∨ (a = b ∈ ℚ))
BY
{ (Auto
   THEN SplitOrHyps
   THEN ThinTrivial
   THEN Try ((OrRight ⋅ THEN Complete (Auto)))
   THEN Try ((OrLeft ⋅ THEN Complete (Auto)))
   THEN Try ((RelRST THEN Complete (Auto)))) }

---

Latex:

---

Latex:

1.  a  :  \mBbbQ{}@i
2.  b  :  \mBbbQ{}@i
3.  a  <  b  \mvee{}  (a  =  b)  \mvee{}  b  <  a
4.  uiff(\mneg{}a  <  b;b  \mleq{}  a)
\mvdash{}  uiff(a  \mleq{}  b;a  <  b  \mvee{}  (a  =  b))


By

---

Latex:
(Auto
  THEN  SplitOrHyps
  THEN  ThinTrivial
  THEN  Try  ((OrRight  \mcdot{}  THEN  Complete  (Auto)))
  THEN  Try  ((OrLeft  \mcdot{}  THEN  Complete  (Auto)))
  THEN  Try  ((RelRST  THEN  Complete  (Auto))))

---

Home Index