---

Step * 2 of Lemma radd-list-rabs


|r0| ≤ r0
BY
{ TACTIC:((RWO "rabs-int" 0 THEN Auto) THEN Unfold `absval` 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

|r0|  \mleq{}  r0


By

---

Latex:
TACTIC:((RWO  "rabs-int"  0  THEN  Auto)  THEN  Unfold  `absval`  0  THEN  Reduce  0  THEN  Auto)

---

Home Index