-- Maclain Hunter: OR Commutativity (magnitude distinct)
-- Exact authored source SHA-256: f8adb9da481011e9f218974a409c94ed6c905eddd1691e67b560e0befa5f9151
-- Machine formalization by Replit Agent; authority below Logic/Logos/God.
import Lean
namespace HunterAuthored

def dominantValue (a b : Int) : Int := if a.natAbs < b.natAbs then b else a
theorem distinct_magnitude_or_commutative (a b : Int) (distinct : a.natAbs ≠ b.natAbs) :
    dominantValue a b = dominantValue b a := by
  unfold dominantValue
  cases Nat.lt_or_gt_of_ne distinct with
  | inl h =>
    rw [if_pos h, if_neg (Nat.not_lt_of_ge (Nat.le_of_lt h))]
  | inr h =>
    rw [if_neg (Nat.not_lt_of_ge (Nat.le_of_lt h)), if_pos h]
#print axioms distinct_magnitude_or_commutative

end HunterAuthored