---

Step * of Lemma sqeq-copath5

∀[n,m:Top].  ((m + 1) - n - 1 ~ m - n - 1 - 1)
BY
{ ((UnivCD THENA Auto) THEN SqEqualTopToBase THEN SqequalSqle THEN AssumeHasValue) }

1
1. n : Base
2. m : Base
3. ((m + 1) - n - 1)↓
⊢ (m + 1) - n - 1 ≤ m - n - 1 - 1

2
1. n : Base
2. m : Base
3. is-exception((m + 1) - n - 1)
⊢ (m + 1) - n - 1 ≤ m - n - 1 - 1

3
1. n : Base
2. m : Base
3. (m - n - 1 - 1)↓
⊢ m - n - 1 - 1 ≤ (m + 1) - n - 1

4
1. n : Base
2. m : Base
3. is-exception(m - n - 1 - 1)
⊢ m - n - 1 - 1 ≤ (m + 1) - n - 1

---

Latex:

---

Latex:
\mforall{}[n,m:Top].    ((m  +  1)  -  n  -  1  \msim{}  m  -  n  -  1  -  1)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  SqEqualTopToBase  THEN  SqequalSqle  THEN  AssumeHasValue)

---

Home Index