---

Step * 1 2 1 of Lemma qadd_grp_wf2


UniformLinorder(ℚ;x,y.↑q_le(x;y))
BY
{ TACTIC:(AGenRepD ["compound";"basic"]
          THEN Auto
          THEN (All (\h. TACTIC:((RWO "q_le-elim" h THENM RW assert_pushdownC h) THENA Auto)))⋅) }

1
1. a : ℚ
⊢ (↑qpositive(a + -(a))) ∨ (a = a ∈ ℚ)

2
1. a : ℚ
2. b : ℚ
3. c : ℚ
4. (↑qpositive(b + -(a))) ∨ (a = b ∈ ℚ)
5. (↑qpositive(c + -(b))) ∨ (b = c ∈ ℚ)
⊢ (↑qpositive(c + -(a))) ∨ (a = c ∈ ℚ)

3
1. x : ℚ
2. y : ℚ
3. (↑qpositive(y + -(x))) ∨ (x = y ∈ ℚ)
4. (↑qpositive(x + -(y))) ∨ (y = x ∈ ℚ)
⊢ x = y ∈ ℚ

4
1. x : ℚ@i
2. y : ℚ@i
⊢ ((↑qpositive(y + -(x))) ∨ (x = y ∈ ℚ)) ∨ (↑qpositive(x + -(y))) ∨ (y = x ∈ ℚ)

---

Latex:

---

Latex:

UniformLinorder(\mBbbQ{};x,y.\muparrow{}q\_le(x;y))


By

---

Latex:
TACTIC:(AGenRepD  ["compound";"basic"]
                THEN  Auto
                THEN  (All  (\mbackslash{}h.  TACTIC:((RWO  "q\_le-elim"  h  THENM  RW  assert\_pushdownC  h)  THENA  Auto)))\mcdot{})

---

Home Index