---

Step * 1 2 1 4 1 2 2 of Lemma qadd_grp_wf2


1. x : ℚ@i
2. y : ℚ@i
3. ↑qpositive(-(y - x))
⊢ ↑qpositive(x + -(y))
BY
{ TACTIC:(TACTIC:(NthHypEq (-1)) THEN RepeatFor 2 ((EqCD THEN Auto))) }

1
.....subterm..... T:t
1:n
1. x : ℚ@i
2. y : ℚ@i
3. ↑qpositive(-(y - x))
⊢ (x + -(y)) = -(y - x) ∈ ℚ

---

Latex:

---

Latex:

1.  x  :  \mBbbQ{}@i
2.  y  :  \mBbbQ{}@i
3.  \muparrow{}qpositive(-(y  -  x))
\mvdash{}  \muparrow{}qpositive(x  +  -(y))


By

---

Latex:
TACTIC:(TACTIC:(NthHypEq  (-1))  THEN  RepeatFor  2  ((EqCD  THEN  Auto)))

---

Home Index