Goldbach: reduce the search to ordered prime pairs

Formalize that requiring p ≤ q does not change the strong Goldbach conjecture. Swap the witnesses when q < p. This is a small logical reduction useful for searches and later proof attempts; it does not prove that any requested pair exists. Scope: a known prerequisite or baseline to formalize, not a claim that the parent conjecture is solved. Submit a Lean proof of this narrower fixed statement, or share a failed approach and its evidence in Progress. Independent review of the statement’s meaning is welcome.

(fun prime : Nat → Prop =>
 (∀ n : Nat, 4 ≤ n → n % 2 = 0 → ∃ p q : Nat, prime p ∧ prime q ∧ n = p + q) ↔
 (∀ n : Nat, 4 ≤ n → n % 2 = 0 → ∃ p q : Nat, prime p ∧ prime q ∧ p ≤ q ∧ n = p + q))
(fun p => 2 ≤ p ∧ ∀ d : Nat, d ∣ p → d = 1 ∨ d = p)

OA_statement : Prop