n✝ m n : ℕ
k : Fin (n + 2)
⊢ (↑k + ↑1) % (n + 2) < ↑k ↔ ↑k = n + 1
n✝ m n : ℕ
k : Fin (n + 2)
⊢ k + 1 < k ↔ k = last (n + 1)
simp only [lt_iff_val_lt_val, val_add, val_last, ext_iff]
case mk
n✝ m n k : ℕ
hk : k < n + 2
⊢ (↑{ val := k, isLt := hk } + ↑1) % (n + 2) < ↑{ val := k, isLt := hk } ↔ ↑{ val := k, isLt := hk } = n + 1
n✝ m n : ℕ
k : Fin (n + 2)
⊢ (↑k + ↑1) % (n + 2) < ↑k ↔ ↑k = n + 1
cases' k with k hk
case mk.inl
n✝ m n : ℕ
hk : n + 1 < n + 2
⊢ (↑{ val := n + 1, isLt := hk } + ↑1) % (n + 2) < ↑{ val := n + 1, isLt := hk } ↔ ↑{ val := n + 1, isLt := hk } = n + 1

case mk.inr
n✝ m n k : ℕ
hk : k < n + 2
hk' : k < n + 1
⊢ (↑{ val := k, isLt := hk } + ↑1) % (n + 2) < ↑{ val := k, isLt := hk } ↔ ↑{ val := k, isLt := hk } = n + 1
case mk
n✝ m n k : ℕ
hk : k < n + 2
⊢ (↑{ val := k, isLt := hk } + ↑1) % (n + 2) < ↑{ val := k, isLt := hk } ↔ ↑{ val := k, isLt := hk } = n + 1
rcases(le_of_lt_succ hk).eq_or_lt with (rfl | hk')
no goals
case mk.inl
n✝ m n : ℕ
hk : n + 1 < n + 2
⊢ (↑{ val := n + 1, isLt := hk } + ↑1) % (n + 2) < ↑{ val := n + 1, isLt := hk } ↔ ↑{ val := n + 1, isLt := hk } = n + 1
simp
no goals
case mk.inr
n✝ m n k : ℕ
hk : k < n + 2
hk' : k < n + 1
⊢ (↑{ val := k, isLt := hk } + ↑1) % (n + 2) < ↑{ val := k, isLt := hk } ↔ ↑{ val := k, isLt := hk } = n + 1
simp [hk'.ne, mod_eq_of_lt (succ_lt_succ hk'), le_succ _]