-- Maclain Hunter: AND Commutativity
-- Exact authored source SHA-256: 1bac6610690928014d0382c506eed874cfb6aef628097814e581ffe09d8bc95a
-- Machine formalization by Replit Agent; authority below Logic/Logos/God.
import Lean
namespace HunterAuthored

def minimumNat : Nat → Nat → Nat
  | 0, _ => 0
  | _, 0 => 0
  | a + 1, b + 1 => minimumNat a b + 1
theorem minimum_commutative (a b : Nat) : minimumNat a b = minimumNat b a := by
  induction a generalizing b with
  | zero => cases b <;> rfl
  | succ a ih =>
    cases b with
    | zero => rfl
    | succ b => exact congrArg Nat.succ (ih b)
def magnitudeAnd (a b : Int) : Int :=
  (if a * b < 0 then -1 else 1) * (minimumNat a.natAbs b.natAbs : Int)
theorem magnitude_and_commutative (a b : Int) : magnitudeAnd a b = magnitudeAnd b a := by
  unfold magnitudeAnd
  rw [Int.mul_comm a b, minimum_commutative a.natAbs b.natAbs]
#print axioms magnitude_and_commutative

end HunterAuthored