mk: peano arithmetic (zeroo, pluso, minuso, *o, lteo, lto)

Classic miniKanren Peano arithmetic on (:z / (:s n)) naturals. pluso runs
relationally in all directions: 2+3=5 forward, x+2=5 → 3 backward,
enumerates the four pairs summing to 3. *o is iterated pluso. lteo/lto
via existential successor decomposition.

19 new tests, 188/188 cumulative. Phase-tagged in the plan separately
from Phase 6 CLP(FD), which will eventually replace this with native
integers + arc-consistency propagation.

plans/minikanren-on-sx.md

@@ -156,6 +156,11 @@ _(none yet)_
 
 _Newest first._
 
+- **2026-05-07** — **Peano arithmetic** (`lib/minikanren/peano.sx`): zeroo, pluso,
+  minuso, lteo, lto, *o on Peano-encoded naturals (`:z` / `(:s n)`). pluso runs
+  forward, backward, and enumerates: `(run* q (fresh (a b) (pluso a b 3)
+  (== q (list a b))))` → all 4 pairs summing to 3. *o uses repeated pluso —
+  works for small inputs, slower for larger. 19 new tests, 188/188 cumulative.
 - **2026-05-07** — **Phase 5 piece A — conda**: soft-cut. Mirrors `condu` minus
   the `onceo` on the head: all head answers are conjuncted through the rest of
   the chosen clause. 7 new tests including the conda-vs-condu divergence test.