---

Step * 1 of Lemma upto_add_1


1. n : ℕ
⊢ upto((n + 1) - 1) @ [(n + 1) - 1] ~ upto(n) @ [n]
BY
{ RepeatFor 2 (EqCD)
THEN Auto }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
\mvdash{}  upto((n  +  1)  -  1)  @  [(n  +  1)  -  1]  \msim{}  upto(n)  @  [n]


By

---

Latex:
RepeatFor  2  (EqCD)
THEN  Auto

---

Home Index