---

Step * 1 2 1 2 1 1 of Lemma qadd_grp_wf2


1. a : ℚ
2. b : ℚ
3. c : ℚ
4. ↑qpositive(b + -(a))
5. ↑qpositive(c + -(b))
⊢ ↑qpositive(c + -(a))
BY
{ TACTIC:(TACTIC:FLemma `qadd_positive` [-1;-2]
          THEN Auto
          THEN TACTIC:(NthHypEq (-1))
          THEN RepeatFor 2 ((EqCD THEN Auto))) }

1
.....subterm..... T:t
1:n
1. a : ℚ
2. b : ℚ
3. c : ℚ
4. ↑qpositive(b + -(a))
5. ↑qpositive(c + -(b))
6. ↑qpositive((c + -(b)) + b + -(a))
⊢ (c + -(a)) = ((c + -(b)) + b + -(a)) ∈ ℚ

---

Latex:

---

Latex:

1.  a  :  \mBbbQ{}
2.  b  :  \mBbbQ{}
3.  c  :  \mBbbQ{}
4.  \muparrow{}qpositive(b  +  -(a))
5.  \muparrow{}qpositive(c  +  -(b))
\mvdash{}  \muparrow{}qpositive(c  +  -(a))


By

---

Latex:
TACTIC:(TACTIC:FLemma  `qadd\_positive`  [-1;-2]
                THEN  Auto
                THEN  TACTIC:(NthHypEq  (-1))
                THEN  RepeatFor  2  ((EqCD  THEN  Auto)))

---

Home Index