---

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


1. x : ℚ@i
2. y : ℚ@i
3. (y - x) = 0 ∈ ℚ
⊢ y = x ∈ ℚ
BY
{ TACTIC:((Assert ((y - x) + x) = (0 + x) ∈ ℚ BY
                 (EqCD THEN Auto))
          THEN TACTIC:(NthHypEq (-1))
          THEN EqCD
          THEN Auto
          THEN QAddReduce 0) }

---

Latex:

---

Latex:

1.  x  :  \mBbbQ{}@i
2.  y  :  \mBbbQ{}@i
3.  (y  -  x)  =  0
\mvdash{}  y  =  x


By

---

Latex:
TACTIC:((Assert  ((y  -  x)  +  x)  =  (0  +  x)  BY
                              (EqCD  THEN  Auto))
                THEN  TACTIC:(NthHypEq  (-1))
                THEN  EqCD
                THEN  Auto
                THEN  QAddReduce  0)

---

Home Index