---

Step * 1 1 of Lemma iterate-rotate


1. n : ℕ
2. x : ℕn@i
3. k : ℕ@i
⊢ x + k rem n ∈ ℕn
BY
{ (InstLemma `rem_bounds_1` [⌜x + k⌝;⌜n⌝]⋅ THEN Auto THEN Auto') }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  x  :  \mBbbN{}n@i
3.  k  :  \mBbbN{}@i
\mvdash{}  x  +  k  rem  n  \mmember{}  \mBbbN{}n


By

---

Latex:
(InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}x  +  k\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THEN  Auto  THEN  Auto')

---

Home Index