---

Step * of Lemma rat-rleq-cases-ext

∀x,y:ℤ × ℕ+.  ((↓ratreal(x) ≤ ratreal(y)) ∨ (↓ratreal(y) ≤ ratreal(x)))
BY
{ Extract of Obid: rat-rleq-cases
  normalizes to:
  
  λx.let x1,x2 = x 
     in λy.let y1,y2 = y 
           in if (y1 * x2) < (x1 * y2)  then inr Ax   else (inl Ax)
  finishing with 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:
Extract  of  Obid:  rat-rleq-cases
normalizes  to:

\mlambda{}x.let  x1,x2  =  x 
      in  \mlambda{}y.let  y1,y2  =  y 
                  in  if  (y1  *  x2)  <  (x1  *  y2)    then  inr  Ax      else  (inl  Ax)
finishing  with  Auto

---

Home Index