fix(proofs/idris2): RMO.idr overwriteIrreversible + auditTrailCompleteness type-sig fixes (#117)

Two single-line type-signature errors in RMO.idr that prevented the
full Idris2 proof tree from building end-to-end. Both surfaced via the
build oracle (#70) once #112 (AuditEntry.proof reserved-keyword fix)
and #113 (hardwareEraseIrreversible single-line signature) cleared the
prior parse errors.

## overwriteIrreversible (line 120)

`length randomData >= length originalContent` is a `Bool` term (since
`(>=)` is Boolean), but a precondition in a function type requires a
`Type`. Replaced with the propositional ordering:

    LTE (length originalContent) (length randomData)

Imports `Data.Nat` for `LTE`. Same fix pattern as `undoRedoComposition`
in PR #109. Body remains `?overwriteIrreversibleProof` (separate proof
debt).

## auditTrailCompleteness (line 252)

`Elem` was undefined (Idris2 0.8.0 lives in `Data.List.Elem`, not
re-exported by `Data.List`). Also `map path entries` was ambiguous
between `Filesystem.Model.Path` (a type) and `AuditEntry.path` (the
record accessor) — qualified to `AuditEntry.path`.

Imports `Data.List.Elem` for `Elem`. Body remains
`?auditTrailCompletenessProof`.

## Net effect

All 4 modules build clean for the first time:

    $ idris2 --build proofs/idris2/valence-shell.ipkg
    1/4: Building Filesystem.Model       OK
    2/4: Building Filesystem.RMO         OK
    3/4: Building Filesystem.Operations  OK
    4/4: Building Filesystem.Composition OK

This unblocks #70's Idris2 build oracle going strict (flip the
workflow's terminal `exit 0` → `exit 1` and add to branch protection's
required checks).

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

Author: hyperpolymath

proofs/idris2/src/Filesystem/RMO.idr

@@ -9,6 +9,8 @@ module Filesystem.RMO
 
 import Filesystem.Model
 import Data.List
+import Data.List.Elem
+import Data.Nat
 
 %default total
 
@@ -117,7 +119,7 @@ overwriteIrreversible :
   (originalContent : FileContent) ->
   (randomData : FileContent) ->
   (fs : Filesystem) ->
-  (length randomData >= length originalContent) ->
+  LTE (length originalContent) (length randomData) ->
   -- After overwrite, original is irrecoverable
   (recovery : FileContent -> Maybe FileContent) ->
   recovery randomData = Nothing  -- Cannot recover original
@@ -249,5 +251,5 @@ auditTrailCompleteness :
   (p : Path) ->
   -- If p was obliterated, it's in the audit log
   (obliterated : ObliterationProof p) ->
-  Elem p (map path entries)  -- p appears in the log
+  Elem p (map AuditEntry.path entries)  -- p appears in the log
 auditTrailCompleteness entries p oblitProof = ?auditTrailCompletenessProof