-- Maclain Hunter: OR Commutativity (magnitude distinct)
-- Exact authored source SHA-256: c468914d86f2d9feb2a549efb6c7ed74b22146a0392c5ce5968ba4ab325c4c9f
-- 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