Splitting off the least index of a finitely supported function

A natural-valued finitely supported function with an index below l in its support splits as single i 1 + g, where i < l and every index in the support of g is at least i. This decomposition supports induction on ordered monomials by removing one occurrence of their least variable.

theorem Finsupp.exists_eq_single_add_of_not_forall_le {ι : Type u_1} [LinearOrder ι] (f : ι →₀ ℕ) {l : ι} (h : ¬∀ i ∈ f.support, l ≤ i) : ∃ (i : ι) (g : ι →₀ ℕ), i < l ∧ (∀ j ∈ g.support, i ≤ j) ∧ f = single i 1 + g

If the support of f is not bounded below by l, split off one occurrence of its least index i < l. Every index in the remaining support is at least i.