---

Step * 1 of Lemma qneginv-positive

.....subterm..... T:t
2:n
1. v : ℚ
2. v < 0
3. (1/v) < 0
4. 0 < -((1/v))
⊢ (-1/v) = -((1/v)) ∈ ℚ
BY
{ (Unfold `qdiv` 0 THEN QNorm 0 THEN RW assert_pushdownC 0 THEN Auto)⋅ }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  v  :  \mBbbQ{}
2.  v  <  0
3.  (1/v)  <  0
4.  0  <  -((1/v))
\mvdash{}  (-1/v)  =  -((1/v))


By

---

Latex:
(Unfold  `qdiv`  0  THEN  QNorm  0  THEN  RW  assert\_pushdownC  0  THEN  Auto)\mcdot{}

---

Home Index