Finsupp.cons_succ

theorem Finsupp.cons_succ : ∀ {n : ℕ} (i : Fin n) {M : Type u_1} [inst : Zero M] (y : M) (s : Fin n →₀ M), (Finsupp.cons y s) i.succ = s i := by sorry

The theorem `Finsupp.cons_succ` states that for any natural number `n`, any element `i` of the finite set `Fin n`, any type `M` with a zero instance, any element `y` of type `M`, and any function `s` from `Fin n` to `M`, applying the function `Finsupp.cons y s` on `Fin.succ i` is equal to `s i`. In other words, this theorem ensures that if you add an element at the beginning of a sequence (which is what `Finsupp.cons` does) and then ask for the successor of some element `i` in the extended sequence, it is the same as asking for the element `i` in the original sequence.

More concisely: For any natural number `n`, any `i` in `Fin n`, any type `M` with a zero instance, any `y` in `M`, and any function `s` from `Fin n` to `M`, `Finsupp.cons y (s i) = s (Fin.succ i)`.