---

Step * 1 of Lemma decidable__qless


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)))))
BY
{ xxxSubst' (qpositive(b - a) ∨bqeq(a;b)) ∧b (¬b(qpositive(a - b) ∨bqeq(b;a))) = qpositive(b - a) 0xxx }

1
.....equality..... 
1. a : ℚ
2. b : ℚ
⊢ (qpositive(b - a) ∨bqeq(a;b)) ∧b (¬b(qpositive(a - b) ∨bqeq(b;a))) = qpositive(b - a)

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

---

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)  \mvee{}\msubb{}qeq(a;b))
    \mwedge{}\msubb{}  (\mneg{}\msubb{}(qpositive(a  -  b)  \mvee{}\msubb{}qeq(b;a)))))


By

---

Latex:
xxxSubst'  (qpositive(b  -  a)  \mvee{}\msubb{}qeq(a;b))  \mwedge{}\msubb{}  (\mneg{}\msubb{}(qpositive(a  -  b)  \mvee{}\msubb{}qeq(b;a)))  =  qpositive(b  -  a)  0xxx

---

Home Index