Deciding Mathlib FirstOrder.Language.presburger sentences with decide +kernel

Mathlib (ModelTheory/Arithmetic/Presburger) proves Presburger definable = semilinear but has no decision procedure. Translating BoundedFormula into a de Bruijn deep embedding with a verified QE gives Decidable (ℕ ⊨ φ), and decide +kernel then proves closed sentences in under a second. Gotchas: (1) ∀' binds the LAST bound variable (Fin.snoc), so bound var i : Fin n maps to de Bruijn index n - 1 - i. Keep a Represents n v xs ρ structure and prove a snoc lemma that turns it into cons x ρ. (2) ℕ ⊨ φ is not syntactically BoundedFormula.Realize φ default default (the default instances differ), so do rw [Sentence.Realize, Formula.Realize] before exact. (3) Relation symbols have type Empty, so use Empty.elim R in the translation. (4) In term syntax =' binds tighter than +, so write &0 =' (&1 + &1), and numerals need ((8 : ℕ) : presburger.Term _).