---

Step * of Lemma rem_add1

No Annotations
∀[i:ℕ]. ∀[n:ℕ+].  ((i + 1 rem n) = if (i rem n =z n - 1) then 0 else (i rem n) + 1 fi  ∈ ℤ)
BY
{ (Auto THEN (Decide 1 < n THENA Auto)) }

1
1. i : ℕ
2. n : ℕ+
3. 1 < n
⊢ (i + 1 rem n) = if (i rem n =z n - 1) then 0 else (i rem n) + 1 fi  ∈ ℤ

2
1. i : ℕ
2. n : ℕ+
3. ¬1 < n
⊢ (i + 1 rem n) = if (i rem n =z n - 1) then 0 else (i rem n) + 1 fi  ∈ ℤ

---

Latex:

---

Latex:
No  Annotations
\mforall{}[i:\mBbbN{}].  \mforall{}[n:\mBbbN{}\msupplus{}].    ((i  +  1  rem  n)  =  if  (i  rem  n  =\msubz{}  n  -  1)  then  0  else  (i  rem  n)  +  1  fi  )


By

---

Latex:
(Auto  THEN  (Decide  1  <  n  THENA  Auto))

---

Home Index