---

Step * of Lemma rat-rleq-cases

∀x,y:ℤ × ℕ+.  ((↓ratreal(x) ≤ ratreal(y)) ∨ (↓ratreal(y) ≤ ratreal(x)))
BY
{ (((RepeatFor 2 (((D 0 THENA Auto) THEN D -1))
     THEN UseWitness ⌜x1 * y2 ≤z y1 * x2⌝⋅
     THEN (BoolCase ⌜x1 * y2 ≤z y1 * x2⌝⋅ THENA Auto)
     THEN Unfolds ``btrue bfalse`` 0
     THEN (MemCD THENA Auto))
    THEN Unfold `it` 0
    THEN MemTypeCD
    THEN (RWO  "ratreal-req" 0 THENA Auto))
   THEN RWO  "rleq-int-fractions" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}.    ((\mdownarrow{}ratreal(x)  \mleq{}  ratreal(y))  \mvee{}  (\mdownarrow{}ratreal(y)  \mleq{}  ratreal(x)))


By

---

Latex:
(((RepeatFor  2  (((D  0  THENA  Auto)  THEN  D  -1))
      THEN  UseWitness  \mkleeneopen{}x1  *  y2  \mleq{}z  y1  *  x2\mkleeneclose{}\mcdot{}
      THEN  (BoolCase  \mkleeneopen{}x1  *  y2  \mleq{}z  y1  *  x2\mkleeneclose{}\mcdot{}  THENA  Auto)
      THEN  Unfolds  ``btrue  bfalse``  0
      THEN  (MemCD  THENA  Auto))
    THEN  Unfold  `it`  0
    THEN  MemTypeCD
    THEN  (RWO    "ratreal-req"  0  THENA  Auto))
  THEN  RWO    "rleq-int-fractions"  0
  THEN  Auto)

---

Home Index