proof(SafeJson): DISCHARGE appendLengthInc via lengthSnoc + plusCommutative

`append v (JsonArray arr) = JsonArray (arr ++ [v])` (SafeJson.idr
L233-234), so the goal reduces to
`Just (length (arr ++ [v])) = Just (length arr + 1)`.

Two-step proof:
1. lengthSnoc arr v : length (arr ++ [v]) = S (length arr)
2. plusCommutative 1 (length arr) : 1 + length arr = length arr + 1
   (where 1 + n = S n by Nat addition)

Combined via `trans` inside `cong Just`:
- appendLengthInc v arr = cong Just (trans (lengthSnoc arr v) (plusCommutative 1 (length arr)))

Adds Data.List.Equalities (contrib, already used by #97 SafeUrl + #124
SafeBuffer) and Data.Nat for plusCommutative.

Surfaced by the post-empirical re-audit (proven#119).

Refs #90 #107 #119

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

src/Proven/SafeJson/Proofs.idr

@@ -9,7 +9,9 @@ module Proven.SafeJson.Proofs
 import Proven.Core
 import Proven.SafeJson
 import Data.List
+import Data.List.Equalities
 import Data.List.Quantifiers
+import Data.Nat
 
 %default total
 
@@ -193,10 +195,17 @@ prependLengthInc v arr = Refl
 ||| `Data.List.lengthAppendSingleton` lemma. Discharge by composing
 ||| `lengthAppend` + `plusZeroRightNeutral` + `S` congruence, or by
 ||| adding a direct singleton-append lemma to base.
-public export
-0 appendLengthInc : (v : JsonValue) -> (arr : List JsonValue) ->
-                            arrayLength (append v (JsonArray arr)) =
-                            Just (length arr + 1)
+||| DISCHARGED: `append v (JsonArray arr) = JsonArray (arr ++ [v])`
+||| (SafeJson.idr L233-234), so the goal reduces to
+||| `Just (length (arr ++ [v])) = Just (length arr + 1)`. Apply
+||| `lengthSnoc arr v : length (arr ++ [v]) = S (length arr)`, then
+||| close the `S n` vs `n + 1` gap with `plusCommutative 1 n`.
+public export
+appendLengthInc : (v : JsonValue) -> (arr : List JsonValue) ->
+                  arrayLength (append v (JsonArray arr)) =
+                  Just (length arr + 1)
+appendLengthInc v arr =
+  cong Just (trans (lengthSnoc arr v) (plusCommutative 1 (length arr)))
 
 --------------------------------------------------------------------------------
 -- Path Access Properties