-- Minimum and maximum of two integers
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Int.MinMax
import AbsoluteValueOrder

theorem integerLess.or_le (x y : Integer)
  shows x < y ∨ y ≤ x
proof
  have split : x < y ∨ ¬x < y by tauto
  cases split with less | notLess
  . left
    exact less
  . right
    exact integerLe.of_not_less with notLess

defunique integerMin (a b : Set) (m ∈ ℤ) :=
  (integerLe(a, b) ∧ m = a) ∨ (integerLess(b, a) ∧ m = b)
requires aInteger : Integer(a)
requires bInteger : Integer(b)
proof
  have split := integerLess.or_le at b, a
  cases split with above | below
  . have bMember : b ∈ ℤ by settle with Integer
    refine ⟨b, bMember, ?_⟩
    right
    exact ⟨above, rfl⟩
  . have aMember : a ∈ ℤ by settle with Integer
    refine ⟨a, aMember, ?_⟩
    left
    exact ⟨below, rfl⟩

uniqueness
  intros m mMember first n nMember second
  cases first with firstLow | firstHigh
  . cases second with secondLow | secondHigh
    . cc
    . exfalso
      exact integerLe.not_less with firstLow.left, secondHigh.left
  . cases second with secondLow | secondHigh
    . exfalso
      exact integerLe.not_less with secondLow.left, firstHigh.left
    . cc

defunique integerMax (a b : Set) (m ∈ ℤ) :=
  (integerLe(a, b) ∧ m = b) ∨ (integerLess(b, a) ∧ m = a)
requires aInteger : Integer(a)
requires bInteger : Integer(b)
proof
  have split := integerLess.or_le at b, a
  cases split with above | below
  . have aMember : a ∈ ℤ by settle with Integer
    refine ⟨a, aMember, ?_⟩
    right
    exact ⟨above, rfl⟩
  . have bMember : b ∈ ℤ by settle with Integer
    refine ⟨b, bMember, ?_⟩
    left
    exact ⟨below, rfl⟩

uniqueness
  intros m mMember first n nMember second
  cases first with firstLow | firstHigh
  . cases second with secondLow | secondHigh
    . cc
    . exfalso
      exact integerLe.not_less with firstLow.left, secondHigh.left
  . cases second with secondLow | secondHigh
    . exfalso
      exact integerLe.not_less with secondLow.left, firstHigh.left
    . cc

theorem integerMin.integer (a b : Integer)
  shows Integer(integerMin(a, b))
proof
  have selected := integerMin.selected at a, b with *
  exact selected.left

theorem integerMax.integer (a b : Integer)
  shows Integer(integerMax(a, b))
proof
  have selected := integerMax.selected at a, b with *
  exact selected.left

theorem integerMin.of_le (a b : Integer)
  requires below : a ≤ b
  shows integerMin(a, b) = a
proof
  have selected := integerMin.selected at a, b with *
  rcases selected with ⟨member, property⟩
  cases property with low | high
  . exact low.right
  . exfalso
    exact integerLe.not_less with below, high.left

theorem integerMin.of_ge (a b : Integer)
  requires above : b ≤ a
  shows integerMin(a, b) = b
proof
  have selected := integerMin.selected at a, b with *
  rcases selected with ⟨member, property⟩
  cases property with low | high
  . have same := integerLe.antisymmetric with low.left, above
    rw low.right
    exact same
  . exact high.right

theorem integerMax.of_le (a b : Integer)
  requires below : a ≤ b
  shows integerMax(a, b) = b
proof
  have selected := integerMax.selected at a, b with *
  rcases selected with ⟨member, property⟩
  cases property with low | high
  . exact low.right
  . exfalso
    exact integerLe.not_less with below, high.left

theorem integerMax.of_ge (a b : Integer)
  requires above : b ≤ a
  shows integerMax(a, b) = a
proof
  have selected := integerMax.selected at a, b with *
  rcases selected with ⟨member, property⟩
  cases property with low | high
  . have same := integerLe.antisymmetric with low.left, above
    rw low.right
    symm
    exact same
  . exact high.right

theorem integerMin.self (a : Integer)
  shows integerMin(a, a) = a
proof
  exact integerMin.of_le with (integerLe.reflexive at a)

theorem integerMax.self (a : Integer)
  shows integerMax(a, a) = a
proof
  exact integerMax.of_le with (integerLe.reflexive at a)

theorem integerMin.commutative (a b : Integer)
  shows integerMin(a, b) = integerMin(b, a)
proof
  have total := integerLe.total at a, b
  cases total with below | above
  . have left := integerMin.of_le with below
    have right := integerMin.of_ge at b, a with below
    rw [left, right]
    rfl
  . have left := integerMin.of_ge with above
    have right := integerMin.of_le at b, a with above
    rw [left, right]
    rfl

theorem integerMax.commutative (a b : Integer)
  shows integerMax(a, b) = integerMax(b, a)
proof
  have total := integerLe.total at a, b
  cases total with below | above
  . have left := integerMax.of_le with below
    have right := integerMax.of_ge at b, a with below
    rw [left, right]
    rfl
  . have left := integerMax.of_ge with above
    have right := integerMax.of_le at b, a with above
    rw [left, right]
    rfl

theorem integerMin.cases (a b : Integer)
  shows integerMin(a, b) = a ∨ integerMin(a, b) = b
proof
  have total := integerLe.total at a, b
  cases total with below | above
  . left
    exact integerMin.of_le with below
  . right
    exact integerMin.of_ge with above

theorem integerMax.cases (a b : Integer)
  shows integerMax(a, b) = a ∨ integerMax(a, b) = b
proof
  have total := integerLe.total at a, b
  cases total with below | above
  . right
    exact integerMax.of_le with below
  . left
    exact integerMax.of_ge with above

theorem integerMin.le_left (a b : Integer)
  shows integerMin(a, b) ≤ a
proof
  have total := integerLe.total at a, b
  cases total with below | above
  . have value101 := integerMin.of_le with below
    rw value101
    exact integerLe.reflexive with *
  . have value102 := integerMin.of_ge with above
    rw value102
    exact above

theorem integerMin.le_right (a b : Integer)
  shows integerMin(a, b) ≤ b
proof
  have total := integerLe.total at a, b
  cases total with below | above
  . have value103 := integerMin.of_le with below
    rw value103
    exact below
  . have value104 := integerMin.of_ge with above
    rw value104
    exact integerLe.reflexive with *

theorem integerMax.ge_left (a b : Integer)
  shows a ≤ integerMax(a, b)
proof
  have total := integerLe.total at a, b
  cases total with below | above
  . have value105 := integerMax.of_le with below
    rw value105
    exact below
  . have value106 := integerMax.of_ge with above
    rw value106
    exact integerLe.reflexive with *

theorem integerMax.ge_right (a b : Integer)
  shows b ≤ integerMax(a, b)
proof
  have total := integerLe.total at a, b
  cases total with below | above
  . have value107 := integerMax.of_le with below
    rw value107
    exact integerLe.reflexive with *
  . have value108 := integerMax.of_ge with above
    rw value108
    exact above

theorem integerMin.le_integerMax (a b : Integer)
  shows integerLe(integerMin(a, b), integerMax(a, b))
proof
  have low := integerMin.le_left at a, b
  have high := integerMax.ge_left at a, b
  exact integerLe.transitive with low, high

theorem integerMin.le_iff (a b c : Integer)
  shows c ≤ integerMin(a, b) ↔ c ≤ a ∧ c ≤ b
proof
  have minNat := integerMin.integer at a, b
  have low := integerMin.le_left at a, b
  have high := integerMin.le_right at a, b
  constructor
  . intro below
    constructor
    . exact integerLe.transitive with below, low
    . exact integerLe.transitive with below, high
  . intro both
    have total := integerLe.total at a, b
    cases total with first | second
    . have value109 := integerMin.of_le with first
      rw value109
      exact both.left
    . have value110 := integerMin.of_ge with second
      rw value110
      exact both.right

theorem integerMin.le_iff_or (a b c : Integer)
  shows integerMin(a, b) ≤ c ↔ a ≤ c ∨ b ≤ c
proof
  have minNat := integerMin.integer at a, b
  constructor
  . intro below
    have split := integerMin.cases at a, b
    cases split with first | second
    . left
      rw ← first
      exact below
    . right
      rw ← second
      exact below
  . intro split
    cases split with first | second
    . have low := integerMin.le_left at a, b
      exact integerLe.transitive with low, first
    . have high := integerMin.le_right at a, b
      exact integerLe.transitive with high, second

theorem integerMax.le_iff (a b c : Integer)
  shows integerMax(a, b) ≤ c ↔ a ≤ c ∧ b ≤ c
proof
  have maxNat := integerMax.integer at a, b
  have low := integerMax.ge_left at a, b
  have high := integerMax.ge_right at a, b
  constructor
  . intro below
    constructor
    . exact integerLe.transitive with low, below
    . exact integerLe.transitive with high, below
  . intro both
    have total := integerLe.total at a, b
    cases total with first | second
    . have value111 := integerMax.of_le with first
      rw value111
      exact both.right
    . have value112 := integerMax.of_ge with second
      rw value112
      exact both.left

theorem integerMax.ge_iff_or (a b c : Integer)
  shows c ≤ integerMax(a, b) ↔ c ≤ a ∨ c ≤ b
proof
  have maxNat := integerMax.integer at a, b
  constructor
  . intro below
    have split := integerMax.cases at a, b
    cases split with first | second
    . left
      rw ← first
      exact below
    . right
      rw ← second
      exact below
  . intro split
    cases split with first | second
    . have low := integerMax.ge_left at a, b
      exact integerLe.transitive with first, low
    . have high := integerMax.ge_right at a, b
      exact integerLe.transitive with second, high

theorem integerMin.lt_iff (a b c : Integer)
  shows c < integerMin(a, b) ↔ c < a ∧ c < b
proof
  have minNat := integerMin.integer at a, b
  have low := integerMin.le_left at a, b
  have high := integerMin.le_right at a, b
  constructor
  . intro below
    constructor
    . exact integerLess.transitive_le with below, low
    . exact integerLess.transitive_le with below, high
  . intro both
    have total := integerLe.total at a, b
    cases total with first | second
    . have value113 := integerMin.of_le with first
      rw value113
      exact both.left
    . have value114 := integerMin.of_ge with second
      rw value114
      exact both.right

theorem integerMax.lt_iff (a b c : Integer)
  shows integerMax(a, b) < c ↔ a < c ∧ b < c
proof
  have maxNat := integerMax.integer at a, b
  have low := integerMax.ge_left at a, b
  have high := integerMax.ge_right at a, b
  constructor
  . intro below
    constructor
    . exact integerLe.transitive_less with low, below
    . exact integerLe.transitive_less with high, below
  . intro both
    have total := integerLe.total at a, b
    cases total with first | second
    . have value115 := integerMax.of_le with first
      rw value115
      exact both.right
    . have value116 := integerMax.of_ge with second
      rw value116
      exact both.left

theorem integerMin.eq_left_iff (a b : Integer)
  shows integerMin(a, b) = a ↔ a ≤ b
proof
  constructor
  . intro same
    have high := integerMin.le_right at a, b
    rw same at high
    exact high
  . intro below
    exact integerMin.of_le with below

theorem integerMin.eq_right_iff (a b : Integer)
  shows integerMin(a, b) = b ↔ b ≤ a
proof
  constructor
  . intro same
    have low := integerMin.le_left at a, b
    rw same at low
    exact low
  . intro above
    exact integerMin.of_ge with above

theorem integerMax.eq_left_iff (a b : Integer)
  shows integerMax(a, b) = a ↔ b ≤ a
proof
  constructor
  . intro same
    have high := integerMax.ge_right at a, b
    rw same at high
    exact high
  . intro above
    exact integerMax.of_ge with above

theorem integerMax.eq_right_iff (a b : Integer)
  shows integerMax(a, b) = b ↔ a ≤ b
proof
  constructor
  . intro same
    have low := integerMax.ge_left at a, b
    rw same at low
    exact low
  . intro below
    exact integerMax.of_le with below

theorem integerMin.monotone (a b c d : Integer)
  requires first : a ≤ c
  requires second : b ≤ d
  shows integerLe(integerMin(a, b), integerMin(c, d))
proof
  have low := integerMin.le_left at a, b
  have high := integerMin.le_right at a, b
  apply integerMin.le_iff.backward
  constructor
  . exact integerLe.transitive with low, first
  . exact integerLe.transitive with high, second

theorem integerMax.monotone (a b c d : Integer)
  requires first : a ≤ c
  requires second : b ≤ d
  shows integerLe(integerMax(a, b), integerMax(c, d))
proof
  have low := integerMax.ge_left at c, d
  have high := integerMax.ge_right at c, d
  apply integerMax.le_iff.backward
  constructor
  . exact integerLe.transitive with first, low
  . exact integerLe.transitive with second, high

theorem integerMin.associative (a b c : Integer)
  shows integerMin(integerMin(a, b), c) = integerMin(a, integerMin(b, c))
proof
  have innerLeft := integerMin.integer at a, b
  have innerRight := integerMin.integer at b, c
  have total := integerLe.total at a, b
  cases total with below | above
  . have value117 := integerMin.of_le with below
    rw value117
    have totalAC := integerLe.total at a, c
    cases totalAC with belowAC | aboveAC
    . have bound : a ≤ integerMin(b, c)
        exact integerMin.le_iff.backward with ⟨below, belowAC⟩
      have value1 := integerMin.of_le with belowAC
      have value2 := integerMin.of_le with bound
      rw [value1, value2]
      rfl
    . have bound : integerMin(b, c) ≤ a
        have inner := integerMin.le_right at b, c
        exact integerLe.transitive with inner, aboveAC
      have value3 := integerMin.of_ge with aboveAC
      have value4 := integerMin.of_ge with bound
      rw [value3, value4]
      have totalBC := integerLe.total at b, c
      cases totalBC with belowBC | aboveBC
      . have value118 := integerMin.of_le with belowBC
        rw value118
        have bound2 : c ≤ b := integerLe.transitive with aboveAC, below
        exact integerLe.antisymmetric with bound2, belowBC
      . have value119 := integerMin.of_ge with aboveBC
        rw value119
        rfl
  . have value120 := integerMin.of_ge with above
    rw value120
    have totalBC := integerLe.total at b, c
    cases totalBC with belowBC | aboveBC
    . have value121 := integerMin.of_le with belowBC
      rw value121
      have value5 := integerMin.of_ge with above
      rw value5
      rfl
    . have value122 := integerMin.of_ge with aboveBC
      rw value122
      have bound : c ≤ a := integerLe.transitive with aboveBC, above
      have value6 := integerMin.of_ge with bound
      rw value6
      rfl

theorem integerMax.associative (a b c : Integer)
  shows integerMax(integerMax(a, b), c) = integerMax(a, integerMax(b, c))
proof
  have innerLeft := integerMax.integer at a, b
  have innerRight := integerMax.integer at b, c
  have total := integerLe.total at a, b
  cases total with below | above
  . have value123 := integerMax.of_le with below
    rw value123
    have totalBC := integerLe.total at b, c
    cases totalBC with belowBC | aboveBC
    . have value124 := integerMax.of_le with belowBC
      rw value124
      have bound : a ≤ c := integerLe.transitive with below, belowBC
      have value7 := integerMax.of_le with bound
      rw value7
      rfl
    . have value125 := integerMax.of_ge with aboveBC
      rw value125
      have value8 := integerMax.of_le with below
      rw value8
      rfl
  . have value126 := integerMax.of_ge with above
    rw value126
    have totalAC := integerLe.total at a, c
    cases totalAC with belowAC | aboveAC
    . have bound : a ≤ integerMax(b, c)
        have inner := integerMax.ge_right at b, c
        exact integerLe.transitive with belowAC, inner
      have value9 := integerMax.of_le with belowAC
      have value10 := integerMax.of_le with bound
      rw [value9, value10]
      have totalBC := integerLe.total at b, c
      cases totalBC with belowBC | aboveBC
      . have value127 := integerMax.of_le with belowBC
        rw value127
        rfl
      . have value128 := integerMax.of_ge with aboveBC
        rw value128
        have bound2 : b ≤ c := integerLe.transitive with above, belowAC
        exact integerLe.antisymmetric with aboveBC, bound2
    . have bound : integerMax(b, c) ≤ a
        exact integerMax.le_iff.backward with ⟨above, aboveAC⟩
      have value11 := integerMax.of_ge with aboveAC
      have value12 := integerMax.of_ge with bound
      rw [value11, value12]
      rfl

theorem integerMin.add_left (a b k : Integer)
  shows integerMin(k + a, k + b) = k + integerMin(a, b)
proof
  have total := integerLe.total at a, b
  cases total with below | above
  . have shifted := integerLe.add_left at a, b, k with below
    have value13 := integerMin.of_le with below
    have value14 := integerMin.of_le with shifted
    rw [value13, value14]
    rfl
  . have shifted := integerLe.add_left at b, a, k with above
    have value15 := integerMin.of_ge with above
    have value16 := integerMin.of_ge with shifted
    rw [value15, value16]
    rfl

theorem integerMin.add_right (a b k : Integer)
  shows integerMin(a + k, b + k) = integerMin(a, b) + k
proof
  have total := integerLe.total at a, b
  cases total with below | above
  . have shifted := integerLe.add_right at a, b, k with below
    have value17 := integerMin.of_le with below
    have value18 := integerMin.of_le with shifted
    rw [value17, value18]
    rfl
  . have shifted := integerLe.add_right at b, a, k with above
    have value19 := integerMin.of_ge with above
    have value20 := integerMin.of_ge with shifted
    rw [value19, value20]
    rfl

theorem integerMax.add_left (a b k : Integer)
  shows integerMax(k + a, k + b) = k + integerMax(a, b)
proof
  have total := integerLe.total at a, b
  cases total with below | above
  . have shifted := integerLe.add_left at a, b, k with below
    have value21 := integerMax.of_le with below
    have value22 := integerMax.of_le with shifted
    rw [value21, value22]
    rfl
  . have shifted := integerLe.add_left at b, a, k with above
    have value23 := integerMax.of_ge with above
    have value24 := integerMax.of_ge with shifted
    rw [value23, value24]
    rfl

theorem integerMax.add_right (a b k : Integer)
  shows integerMax(a + k, b + k) = integerMax(a, b) + k
proof
  have total := integerLe.total at a, b
  cases total with below | above
  . have shifted := integerLe.add_right at a, b, k with below
    have value25 := integerMax.of_le with below
    have value26 := integerMax.of_le with shifted
    rw [value25, value26]
    rfl
  . have shifted := integerLe.add_right at b, a, k with above
    have value27 := integerMax.of_ge with above
    have value28 := integerMax.of_ge with shifted
    rw [value27, value28]
    rfl

theorem integerMin.add_one (a b : Integer)
  shows integerMin(a + 1, b + 1) = integerMin(a, b) + 1
proof
  exact integerMin.add_right at a, b, integerOne

theorem integerMax.add_one (a b : Integer)
  shows integerMax(a + 1, b + 1) = integerMax(a, b) + 1
proof
  exact integerMax.add_right at a, b, integerOne

theorem integerMin.add_integerMax (a b : Integer)
  shows integerMin(a, b) + integerMax(a, b) = a + b
proof
  have total := integerLe.total at a, b
  cases total with below | above
  . have value129 := integerMin.of_le with below
    have value130 := integerMax.of_le with below
    rw [value129, value130]
    rfl
  . have value131 := integerMin.of_ge with above
    have value132 := integerMax.of_ge with above
    rw [value131, value132]
    ring

theorem integerMax.distribute_integerMin (a b c : Integer)
  shows
    integerMax(a, integerMin(b, c)) =
      integerMin(integerMax(a, b), integerMax(a, c))
proof
  have leftNat := integerMax.integer at a, b
  have rightNat := integerMax.integer at a, c
  have reflexive := integerLe.reflexive at a
  have total := integerLe.total at b, c
  cases total with below | above
  . have outer := integerMax.monotone at a, b, a, c with reflexive, below
    have value45 := integerMin.of_le with below
    have value46 := integerMin.of_le with outer
    rw [value45, value46]
    rfl
  . have outer := integerMax.monotone at a, c, a, b with reflexive, above
    have value47 := integerMin.of_ge with above
    have value48 := integerMin.of_ge with outer
    rw [value47, value48]
    rfl

theorem integerMin.distribute_integerMax (a b c : Integer)
  shows
    integerMin(a, integerMax(b, c)) =
      integerMax(integerMin(a, b), integerMin(a, c))
proof
  have leftNat := integerMin.integer at a, b
  have rightNat := integerMin.integer at a, c
  have reflexive := integerLe.reflexive at a
  have total := integerLe.total at b, c
  cases total with below | above
  . have outer := integerMin.monotone at a, b, a, c with reflexive, below
    have value49 := integerMax.of_le with below
    have value50 := integerMax.of_le with outer
    rw [value49, value50]
    rfl
  . have outer := integerMin.monotone at a, c, a, b with reflexive, above
    have value51 := integerMax.of_ge with above
    have value52 := integerMax.of_ge with outer
    rw [value51, value52]
    rfl

theorem integerMin.absorb_integerMax (a b : Integer)
  shows integerMin(a, integerMax(a, b)) = a
proof
  have high := integerMax.ge_left at a, b
  exact integerMin.of_le with high

theorem integerMax.absorb_integerMin (a b : Integer)
  shows integerMax(a, integerMin(a, b)) = a
proof
  have low := integerMin.le_left at a, b
  exact integerMax.of_ge with low

theorem integerMin.mul_left (a b k : Integer)
  requires nonnegative : 0 ≤ k
  shows integerMin(k * a, k * b) = k * integerMin(a, b)
proof
  have total := integerLe.total at a, b
  cases total with below | above
  . have scaled := integerLe.mul_left at a, b, k with nonnegative, below
    have value1 := integerMin.of_le with below
    have value2 := integerMin.of_le with scaled
    rw [value1, value2]
    rfl
  . have scaled := integerLe.mul_left at b, a, k with nonnegative, above
    have value1 := integerMin.of_ge with above
    have value2 := integerMin.of_ge with scaled
    rw [value1, value2]
    rfl

theorem integerMax.mul_left (a b k : Integer)
  requires nonnegative : 0 ≤ k
  shows integerMax(k * a, k * b) = k * integerMax(a, b)
proof
  have total := integerLe.total at a, b
  cases total with below | above
  . have scaled := integerLe.mul_left at a, b, k with nonnegative, below
    have value1 := integerMax.of_le with below
    have value2 := integerMax.of_le with scaled
    rw [value1, value2]
    rfl
  . have scaled := integerLe.mul_left at b, a, k with nonnegative, above
    have value1 := integerMax.of_ge with above
    have value2 := integerMax.of_ge with scaled
    rw [value1, value2]
    rfl

theorem integerMin.neg (a b : Integer)
  shows integerMin(-a, -b) = -integerMax(a, b)
proof
  have total := integerLe.total at a, b
  cases total with below | above
  . have flipped := integerLe.neg.forward with below
    have value1 := integerMin.of_ge at -a, -b with flipped
    have value2 := integerMax.of_le with below
    rw [value1, value2]
    rfl
  . have flipped := integerLe.neg.forward with above
    have value1 := integerMin.of_le at -a, -b with flipped
    have value2 := integerMax.of_ge with above
    rw [value1, value2]
    rfl

theorem integerMax.neg (a b : Integer)
  shows integerMax(-a, -b) = -integerMin(a, b)
proof
  have total := integerLe.total at a, b
  cases total with below | above
  . have flipped := integerLe.neg.forward with below
    have value1 := integerMax.of_ge at -a, -b with flipped
    have value2 := integerMin.of_le with below
    rw [value1, value2]
    rfl
  . have flipped := integerLe.neg.forward with above
    have value1 := integerMax.of_le at -a, -b with flipped
    have value2 := integerMin.of_ge with above
    rw [value1, value2]
    rfl

theorem integerAbs.eq_integerMax (z : Integer)
  shows integerAbs(z) = integerMax(z, -z)
proof
  have split := integerLe.cases_sign at z
  cases split with nonnegative | nonpositive
  . have value := integerAbs.of_nonneg with nonnegative
    have negated := integerLe.neg_nonneg_iff.forward at z
    have flipped : -z ≤ z
      have bound := integerLe.neg.forward with nonnegative
      have zero : -integerZero = integerZero by ring
      rw zero at bound
      exact integerLe.transitive with bound, nonnegative
    have maxValue := integerMax.of_ge at z, -z with flipped
    rw [value, maxValue]
    rfl
  . have value := integerAbs.of_nonpos with nonpositive
    have flipped : z ≤ -z
      have bound := integerLe.neg.forward with nonpositive
      have zero : -integerZero = integerZero by ring
      rw zero at bound
      exact integerLe.transitive with nonpositive, bound
    have maxValue := integerMax.of_le at z, -z with flipped
    rw [value, maxValue]
    rfl

theorem integerMin.le_integerAbs (z : Integer)
  shows integerMin(z, -z) ≤ integerAbs(z)
proof
  have negatedAbs := integerAbs.neg at z
  have low := integerMin.le_left at z, -z
  have bound := integerAbs.le_self at z
  exact integerLe.transitive with low, bound