---

Step * 1 2 2 1 1 1 of Lemma qadd_grp_wf2


1. x : ℚ@i
2. y : ℚ@i
⊢ x = y ∈ ℚ ⇐⇒ (↑q_le(x;y)) ∧ (↑q_le(y;x))
BY
{ TACTIC:((TACTIC:RWO "q_le-elim" 0 THENA Auto) THEN AutoBoolCase ⌜qeq(x;y)⌝⋅ THEN Auto) }

1
1. x : ℚ@i
2. y : ℚ@i
3. ¬(x = y ∈ ℚ)
4. ↑(qpositive(y + -(x)) ∨bff)
5. ↑(qpositive(x + -(y)) ∨bqeq(y;x))
⊢ x = y ∈ ℚ

---

Latex:

---

Latex:

1.  x  :  \mBbbQ{}@i
2.  y  :  \mBbbQ{}@i
\mvdash{}  x  =  y  \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}q\_le(x;y))  \mwedge{}  (\muparrow{}q\_le(y;x))


By

---

Latex:
TACTIC:((TACTIC:RWO  "q\_le-elim"  0  THENA  Auto)  THEN  AutoBoolCase  \mkleeneopen{}qeq(x;y)\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index