---

Step * 3 1 of Lemma sqeq-copath5


1. n : Base
2. m : Base
3. ((m + (-(n + (-1)))) + (-1))↓
4. m + (-(n + (-1))) ∈ ℤ
5. -1 ∈ ℤ
6. (m + (-(n + (-1))))↓
7. m ∈ ℤ
8. -(n + (-1)) ∈ ℤ
9. (-(n + (-1)))↓
10. n + (-1) ∈ ℤ
11. (n + (-1))↓
12. n ∈ ℤ
13. -1 ∈ ℤ
⊢ (m + (-(n + (-1)))) + (-1) ≤ ((m + 1) + (-n)) + (-1)
BY
{ (Subst ⌜((m + (-(n + (-1)))) + (-1)) = (((m + 1) + (-n)) + (-1)) ∈ ℤ⌝ 0⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  Base
2.  m  :  Base
3.  ((m  +  (-(n  +  (-1))))  +  (-1))\mdownarrow{}
4.  m  +  (-(n  +  (-1)))  \mmember{}  \mBbbZ{}
5.  -1  \mmember{}  \mBbbZ{}
6.  (m  +  (-(n  +  (-1))))\mdownarrow{}
7.  m  \mmember{}  \mBbbZ{}
8.  -(n  +  (-1))  \mmember{}  \mBbbZ{}
9.  (-(n  +  (-1)))\mdownarrow{}
10.  n  +  (-1)  \mmember{}  \mBbbZ{}
11.  (n  +  (-1))\mdownarrow{}
12.  n  \mmember{}  \mBbbZ{}
13.  -1  \mmember{}  \mBbbZ{}
\mvdash{}  (m  +  (-(n  +  (-1))))  +  (-1)  \mleq{}  ((m  +  1)  +  (-n))  +  (-1)


By

---

Latex:
(Subst  \mkleeneopen{}((m  +  (-(n  +  (-1))))  +  (-1))  =  (((m  +  1)  +  (-n))  +  (-1))\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index