Finset.box_succ_eq_sdiff

theorem Finset.box_succ_eq_sdiff : ∀ {α : Type u_1} [inst : OrderedRing α] [inst_1 : LocallyFiniteOrder α] [inst_2 : DecidableEq α] (n : ℕ), Finset.box (n + 1) = Finset.Icc (-↑n.succ) ↑n.succ \ Finset.Icc (-↑n) ↑n

The theorem `Finset.box_succ_eq_sdiff` states that for any given natural number `n` and any type `α` that is an ordered ring with a locally finite order and decidable equality, the hollow box centered at `0` going from `-n-1` to `n+1` (represented by `Finset.box (n + 1)`) is equivalent to the set difference of the interval from `-n-1` to `n+1` and the interval from `-n` to `n` (represented by `Finset.Icc (-↑(Nat.succ n)) ↑(Nat.succ n) \ Finset.Icc (-↑n) ↑n`). In other words, the hollow box at the `n+1` level is formed by removing the box at the `n` level from the solid box at the `n+1` level.

More concisely: For any ordered ring type `α` with locally finite order and decidable equality, the hollow box `Finset.box (Nat.succ n)` centered at `0` in `Finset (α)` is equal to the set difference of the interval `Finset.Icc (-↑(Nat.succ n)) ↑(Nat.succ n)` and the interval `Finset.Icc (-↑n) ↑n` in `Finset (α)`.