---

Step * 1 of Lemma sqeq-copath5


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

1
1. n : Base
2. m : Base
3. (((m + 1) + (-n)) + (-1))↓
4. (m + 1) + (-n) ∈ ℤ
5. -1 ∈ ℤ
6. ((m + 1) + (-n))↓
7. m + 1 ∈ ℤ
8. -n ∈ ℤ
9. (m + 1)↓
10. m ∈ ℤ
11. 1 ∈ ℤ
12. (-n)↓
13. n ∈ ℤ
⊢ ((m + 1) + (-n)) + (-1) ≤ (m + (-(n + (-1)))) + (-1)

---

Latex:

---

Latex:

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


By

---

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

---

Home Index