proof(SafeBuffer): DISCHARGE writeAddsOne + writeManyAddsLength via contrib lemmas (proven#90 #107 #119) (#124)

\`\`\`idris
writeAddsOne x buf buf' prf with (isFull buf)
  writeAddsOne x buf buf' prf | True  = case prf of Refl impossible
writeAddsOne x buf buf' prf | False = case prf of Refl => lengthSnoc
buf.content x

writeManyAddsLength xs buf buf' prf with (length xs > remaining buf)
writeManyAddsLength xs buf buf' prf | True = case prf of Refl impossible
writeManyAddsLength xs buf buf' prf | False = case prf of Refl =>
lengthDistributesOverAppend buf.content xs
\`\`\`

Same `with`-pattern as the existing \`writePreservesCapacity\` and
\`copyToPreservesDestCapacity\` in this file. Uses contrib's
\`Data.List.Equalities.lengthSnoc\` (proven#97 precedent) and
\`lengthDistributesOverAppend\`.

Adds `import Data.List.Equalities` (already used in #97 SafeUrl).

Surfaced by the post-empirical re-audit (proven#119) as a
HIGH-confidence candidate. The OWED comment said the proof was "blocked
on the cons-distribution lemma family" — but those lemmas exist in
contrib's `Data.List.Equalities`, just unused.

Refs #90 #107 #119

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

Author: hyperpolymath

src/Proven/SafeBuffer/Proofs.idr

@@ -42,6 +42,7 @@ module Proven.SafeBuffer.Proofs
 
 import Proven.SafeBuffer
 import Data.List
+import Data.List.Equalities
 import Data.Vect
 
 %default total
@@ -142,16 +143,28 @@ emptyBufferSize (S k) d = cong S (emptyBufferSize k d)
 -- not silent.
 --------------------------------------------------------------------------------
 
-||| OWED: `write` extends content by exactly one. The structural fact is
-||| obvious; the proof is blocked on the cons-distribution lemma family.
+||| DISCHARGED: `write` extends content by exactly one. With-pattern
+||| on `isFull buf`: `True` arm has `Nothing = Just buf'` (impossible);
+||| `False` arm gives `buf' = MkDynBuffer cap (content ++ [x])`, so
+||| `dynLength buf' = length (content ++ [x]) = S (length content)`
+||| via `Data.List.Equalities.lengthSnoc` from contrib.
 public export
-0 writeAddsOne :
+writeAddsOne :
   (x : a) -> (buf : DynBuffer a) -> (buf' : DynBuffer a)
   -> write x buf = Just buf' -> dynLength buf' = S (dynLength buf)
-
-||| OWED: `writeMany` extends content by `length xs`. Same blocker as
-||| `writeAddsOne` (cons-distribution / append-length lemma).
+writeAddsOne x buf buf' prf with (isFull buf)
+  writeAddsOne x buf buf' prf | True  = case prf of Refl impossible
+  writeAddsOne x buf buf' prf | False = case prf of Refl => lengthSnoc buf.content x
+
+||| DISCHARGED: `writeMany` extends content by `length xs`. Same
+||| with-pattern on `length xs > remaining buf`. `False` arm gives
+||| `buf' = MkDynBuffer cap (content ++ xs)`, so
+||| `dynLength buf' = length (content ++ xs) = length content + length xs`
+||| via `Data.List.Equalities.lengthDistributesOverAppend` from contrib.
 public export
-0 writeManyAddsLength :
+writeManyAddsLength :
   (xs : List a) -> (buf : DynBuffer a) -> (buf' : DynBuffer a)
   -> writeMany xs buf = Just buf' -> dynLength buf' = dynLength buf + length xs
+writeManyAddsLength xs buf buf' prf with (length xs > remaining buf)
+  writeManyAddsLength xs buf buf' prf | True  = case prf of Refl impossible
+  writeManyAddsLength xs buf buf' prf | False = case prf of Refl => lengthDistributesOverAppend buf.content xs