proof(SafeJson): DISCHARGE appendLengthInc via lengthSnoc + plusCommutative (proven#90 #107 #119) (#127)

\`\`\`idris
appendLengthInc v arr = cong Just (trans (lengthSnoc arr v)
(plusCommutative 1 (length arr)))
\`\`\`

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

Combined via \`trans\` inside \`cong Just\`.

Adds \`Data.List.Equalities\` (already used by #97 SafeUrl + #124
SafeBuffer) and \`Data.Nat\`.

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