---

Step * 1 4 1 of Lemma rneq-rabs

.....rewrite subgoal..... 
1. a : ℝ
2. v : ℝ
3. a < v
4. a < -(v)
⊢ a ≤ r0
BY
{ ((nRMul ⌜r(-1)⌝ (-2)⋅ THENA Auto) THEN (nRMul ⌜r(-1)⌝ (-1)⋅ THENA Auto) THEN (nRMul ⌜r(-1)⌝ 0⋅ THENA Auto)) }

1
1. a : ℝ
2. v : ℝ
3. -(v) < -(a)
4. v < -(a)
⊢ r0 ≤ -(a)

---

Latex:

---

Latex:
.....rewrite  subgoal..... 
1.  a  :  \mBbbR{}
2.  v  :  \mBbbR{}
3.  a  <  v
4.  a  <  -(v)
\mvdash{}  a  \mleq{}  r0


By

---

Latex:
((nRMul  \mkleeneopen{}r(-1)\mkleeneclose{}  (-2)\mcdot{}  THENA  Auto)
  THEN  (nRMul  \mkleeneopen{}r(-1)\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  (nRMul  \mkleeneopen{}r(-1)\mkleeneclose{}  0\mcdot{}  THENA  Auto))

---

Home Index