---

Step * of Lemma decidable__qle

∀a,b:ℚ.  Dec(a ≤ b)
BY
{ ((UnivCD THENA Auto)
   THEN UseWitness ⌜if qpositive(b - a) ∨bqeq(a;b) then tt else inr (λx.⋅)  fi ⌝⋅
   THEN RepUR ``qle grp_leq  q_le`` 0
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN (BLemma `member-decide-assert` THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbQ{}.    Dec(a  \mleq{}  b)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  UseWitness  \mkleeneopen{}if  qpositive(b  -  a)  \mvee{}\msubb{}qeq(a;b)  then  tt  else  inr  (\mlambda{}x.\mcdot{})    fi  \mkleeneclose{}\mcdot{}
  THEN  RepUR  ``qle  grp\_leq    q\_le``  0
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  (BLemma  `member-decide-assert`  THEN  Auto)\mcdot{})

---

Home Index