---

Step * 2 1 1 1 of Lemma rotate-by-id


1. n : ℕ
2. i : ℕ
3. x : ℕn
4. (i rem n) = 0 ∈ ℤ
5. ((x rem n) + 0 rem n) = (x + i rem n) ∈ ℤ
⊢ ((x rem n) + 0 rem n) = x ∈ ℕn
BY
{ xxx(Symmetry THEN EqTypeCD THEN Auto THEN RepeatFor 2 ((RWW "rem_base_case" 0 THEN Auto)))xxx }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  i  :  \mBbbN{}
3.  x  :  \mBbbN{}n
4.  (i  rem  n)  =  0
5.  ((x  rem  n)  +  0  rem  n)  =  (x  +  i  rem  n)
\mvdash{}  ((x  rem  n)  +  0  rem  n)  =  x


By

---

Latex:
xxx(Symmetry  THEN  EqTypeCD  THEN  Auto  THEN  RepeatFor  2  ((RWW  "rem\_base\_case"  0  THEN  Auto)))xxx

---

Home Index