---

Step * 1 2 1 3 1 of Lemma qadd_grp_wf2


1. x : ℚ
2. y : ℚ
3. ↑qpositive(y + -(x))
4. ↑qpositive(x + -(y))
⊢ x = y ∈ ℚ
BY
{ TACTIC:(TACTIC:(FLemma `qminus_positive` [-2] THENA Auto)
          THEN D -1
          THEN TACTIC:(NthHypEq (-1))
          THEN RepeatFor 2 ((EqCD THEN Auto))) }

---

Latex:

---

Latex:

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


By

---

Latex:
TACTIC:(TACTIC:(FLemma  `qminus\_positive`  [-2]  THENA  Auto)
                THEN  D  -1
                THEN  TACTIC:(NthHypEq  (-1))
                THEN  RepeatFor  2  ((EqCD  THEN  Auto)))

---

Home Index