case mk.zero
n✝ m n : ℕ
hk : zero < n + 2
⊢ { val := zero, isLt := hk } < { val := zero, isLt := hk } - 1 ↔ { val := zero, isLt := hk } = 0

case mk.succ
n✝ m n k : ℕ
hk : Nat.succ k < n + 2
⊢ { val := Nat.succ k, isLt := hk } < { val := Nat.succ k, isLt := hk } - 1 ↔ { val := Nat.succ k, isLt := hk } = 0
n✝ m n : ℕ
k : Fin (n + 2)
⊢ k < k - 1 ↔ k = 0
rcases k with ⟨_ | k, hk⟩
case mk.succ
n✝ m n k : ℕ
hk : Nat.succ k < n + 2
⊢ { val := Nat.succ k, isLt := hk } < { val := Nat.succ k, isLt := hk } - 1 ↔ { val := Nat.succ k, isLt := hk } = 0
case mk.zero
n✝ m n : ℕ
hk : zero < n + 2
⊢ { val := zero, isLt := hk } < { val := zero, isLt := hk } - 1 ↔ { val := zero, isLt := hk } = 0

case mk.succ
n✝ m n k : ℕ
hk : Nat.succ k < n + 2
⊢ { val := Nat.succ k, isLt := hk } < { val := Nat.succ k, isLt := hk } - 1 ↔ { val := Nat.succ k, isLt := hk } = 0
simp [lt_iff_val_lt_val]
case mk.succ
n✝ m n k : ℕ
hk : Nat.succ k < n + 2
this : (k + 1 + (n + 1)) % (n + 2) = k % (n + 2)
⊢ { val := Nat.succ k, isLt := hk } < { val := Nat.succ k, isLt := hk } - 1 ↔ { val := Nat.succ k, isLt := hk } = 0
case mk.succ
n✝ m n k : ℕ
hk : Nat.succ k < n + 2
⊢ { val := Nat.succ k, isLt := hk } < { val := Nat.succ k, isLt := hk } - 1 ↔ { val := Nat.succ k, isLt := hk } = 0
have : (k + 1 + (n + 1)) % (n + 2) = k % (n + 2) := by
  rw [add_right_comm, add_assoc, add_mod_right]
no goals
case mk.succ
n✝ m n k : ℕ
hk : Nat.succ k < n + 2
this : (k + 1 + (n + 1)) % (n + 2) = k % (n + 2)
⊢ { val := Nat.succ k, isLt := hk } < { val := Nat.succ k, isLt := hk } - 1 ↔ { val := Nat.succ k, isLt := hk } = 0
simp [lt_iff_val_lt_val, ext_iff, Fin.coe_sub, succ_eq_add_one, this,
  mod_eq_of_lt ((lt_succ_self _).trans hk)]
no goals
n✝ m n k : ℕ
hk : Nat.succ k < n + 2
⊢ (k + 1 + (n + 1)) % (n + 2) = k % (n + 2)
rw [add_right_comm, add_assoc, add_mod_right]