---

Step * 1 of Lemma iterate-rotate

.....assertion..... 
1. n : ℕ
⊢ ∀x:ℕn. ∀k:ℕ.  (x + k rem n ∈ ℕn)
BY
{ TACTIC:(UnivCD THENA Auto) }

1
1. n : ℕ
2. x : ℕn@i
3. k : ℕ@i
⊢ x + k rem n ∈ ℕn

---

Latex:

---

Latex:
.....assertion..... 
1.  n  :  \mBbbN{}
\mvdash{}  \mforall{}x:\mBbbN{}n.  \mforall{}k:\mBbbN{}.    (x  +  k  rem  n  \mmember{}  \mBbbN{}n)


By

---

Latex:
TACTIC:(UnivCD  THENA  Auto)

---

Home Index