proof(coq): FunctionalExtensionality to posix_errors + rmo; Omega→Lia

Complete FunctionalExtensionality import sweep.
Replace deprecated Require Import Omega with Lia in rmo_operations.v.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: hyperpolymath

proofs/coq/posix_errors.v

@@ -17,6 +17,8 @@ Require Import List.
 Require Import Bool.
 Import ListNotations.
 
+Require Import Coq.Logic.FunctionalExtensionality.
+
 Require Import filesystem_model.
 Require Import file_operations.
 Require Import filesystem_composition.

proofs/coq/rmo_operations.v

@@ -22,7 +22,8 @@ Require Import String.
 Require Import List.
 Require Import Bool.
 Require Import Arith.
-Require Import Omega.
+Require Import Lia.
+Require Import Coq.Logic.FunctionalExtensionality.
 Import ListNotations.
 
 (* Import base filesystem model *)