---

Step * 1 2 of Lemma decidable__qless


1. a : ℚ
2. b : ℚ
⊢ if qpositive(b - a) then tt else inr (λx.⋅)  fi  ∈ Dec(↑qpositive(b - a))
BY
{ xxx(BLemma `member-decide-assert`  THEN Auto)xxx }

---

Latex:

---

Latex:

1.  a  :  \mBbbQ{}
2.  b  :  \mBbbQ{}
\mvdash{}  if  qpositive(b  -  a)  then  tt  else  inr  (\mlambda{}x.\mcdot{})    fi    \mmember{}  Dec(\muparrow{}qpositive(b  -  a))


By

---

Latex:
xxx(BLemma  `member-decide-assert`    THEN  Auto)xxx

---

Home Index