---

Step * 3 of Lemma sqeq-copath5


1. n : Base
2. m : Base
3. (m - n - 1 - 1)↓
⊢ m - n - 1 - 1 ≤ (m + 1) - n - 1
BY
{ (All(RepUR ``subtract``)
   THEN HasValueD (-1)
   THEN (Assert ⌜(m + (-(n + (-1))))↓⌝⋅ THENA Auto)
   THEN HasValueD (-1)
   THEN (Assert ⌜(-(n + (-1)))↓⌝⋅ THENA Auto)
   THEN HasValueD (-1)
   THEN (Assert ⌜(n + (-1))↓⌝⋅ THENA Auto)
   THEN HasValueD (-1)) }

1
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)

---

Latex:

---

Latex:

1.  n  :  Base
2.  m  :  Base
3.  (m  -  n  -  1  -  1)\mdownarrow{}
\mvdash{}  m  -  n  -  1  -  1  \mleq{}  (m  +  1)  -  n  -  1


By

---

Latex:
(All(RepUR  ``subtract``)
  THEN  HasValueD  (-1)
  THEN  (Assert  \mkleeneopen{}(m  +  (-(n  +  (-1))))\mdownarrow{}\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  HasValueD  (-1)
  THEN  (Assert  \mkleeneopen{}(-(n  +  (-1)))\mdownarrow{}\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  HasValueD  (-1)
  THEN  (Assert  \mkleeneopen{}(n  +  (-1))\mdownarrow{}\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  HasValueD  (-1))

---

Home Index