---

Step * of Lemma decidable__qless

∀a,b:ℚ.  Dec(a < b)
BY
{ ((xxxUnivCDxxx THENA Auto)
   THEN UseWitness ⌜if qpositive(b - a) then tt else inr (λx.⋅)  fi ⌝⋅
   THEN RepUR ``qless grp_lt oset_of_ocmon dset_of_mon set_lt set_blt q_le`` 0
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))) }

1
1. a : ℚ
2. b : ℚ
⊢ if qpositive(b - a) then tt else inr (λx.⋅)  fi  ∈ Dec(↑((qpositive(b - a) ∨bqeq(a;b))
  ∧b (¬b(qpositive(a - b) ∨bqeq(b;a)))))

---

Latex:

---

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


By

---

Latex:
((xxxUnivCDxxx  THENA  Auto)
  THEN  UseWitness  \mkleeneopen{}if  qpositive(b  -  a)  then  tt  else  inr  (\mlambda{}x.\mcdot{})    fi  \mkleeneclose{}\mcdot{}
  THEN  RepUR  ``qless  grp\_lt  oset\_of\_ocmon  dset\_of\_mon  set\_lt  set\_blt  q\_le``  0
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto)))

---

Home Index