---

Step * of Lemma q_le-elim

∀[r,s:ℚ].  (q_le(r;s) ~ qpositive(s + -(r)) ∨bqeq(r;s))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN RW (AddrC [1] UnfoldTopAbC) 0
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN Unfold `qsub` 0
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[r,s:\mBbbQ{}].    (q\_le(r;s)  \msim{}  qpositive(s  +  -(r))  \mvee{}\msubb{}qeq(r;s))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  RW  (AddrC  [1]  UnfoldTopAbC)  0
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  Unfold  `qsub`  0
  THEN  Trivial)

---

Home Index