---

Step * of Lemma qabs-neg

∀[r:ℚ]. (|-(r)| = |r| ∈ ℚ)
BY
{ (Auto
   THEN ((Unfold `qabs` 0 THEN (CallByValueReduce 0 THENA Auto)) THENM InstLemma `q_trichotomy` [⌜r⌝]⋅)
   THEN Auto
   THEN ((RWO "assert-qpositive" (-1))⋅ THENA Auto)
   THEN ((RWO "qminus-positive" (-1))⋅ THENA Auto)
   THEN RepeatFor 2 (AutoSplit)
   THEN All (RWO "qminus-positive")
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[r:\mBbbQ{}].  (|-(r)|  =  |r|)


By

---

Latex:
(Auto
  THEN  ((Unfold  `qabs`  0  THEN  (CallByValueReduce  0  THENA  Auto))
  THENM  InstLemma  `q\_trichotomy`  [\mkleeneopen{}r\mkleeneclose{}]\mcdot{}
  )
  THEN  Auto
  THEN  ((RWO  "assert-qpositive"  (-1))\mcdot{}  THENA  Auto)
  THEN  ((RWO  "qminus-positive"  (-1))\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (AutoSplit)
  THEN  All  (RWO  "qminus-positive")
  THEN  Auto)

---

Home Index