-- Minimum and maximum of two natural numbers
-- 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.Nat.MinMax
import OrderLemmas

defunique natMin (a b : Nat) (m ∈ ℕ) :=
  (a ≤ b ∧ m = a) ∨ (b < a ∧ m = b)
proof
  have split := Less.or_LessEqual at b, a
  cases split with above | below
  . refine ⟨b, nat.omega.forward at b with *, ?_⟩
    right
    exact ⟨above, rfl⟩
  . refine ⟨a, nat.omega.forward at a with *, ?_⟩
    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 LessEqual.not_Less with firstLow.left, secondHigh.left
  . cases second with secondLow | secondHigh
    . exfalso
      exact LessEqual.not_Less with secondLow.left, firstHigh.left
    . cc

defunique natMax (a b : Nat) (m ∈ ℕ) :=
  (a ≤ b ∧ m = b) ∨ (b < a ∧ m = a)
proof
  have split := Less.or_LessEqual at b, a
  cases split with above | below
  . refine ⟨a, nat.omega.forward at a with *, ?_⟩
    right
    exact ⟨above, rfl⟩
  . refine ⟨b, nat.omega.forward at b with *, ?_⟩
    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 LessEqual.not_Less with firstLow.left, secondHigh.left
  . cases second with secondLow | secondHigh
    . exfalso
      exact LessEqual.not_Less with secondLow.left, firstHigh.left
    . cc

theorem natMin.natural (a b : Nat)
  shows Nat(natMin(a, b))
proof
  have selected := natMin.selected at a, b with *
  exact nat.omega.backward with selected.left

theorem natMax.natural (a b : Nat)
  shows Nat(natMax(a, b))
proof
  have selected := natMax.selected at a, b with *
  exact nat.omega.backward with selected.left

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

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

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

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

theorem natMin.self (a : Nat)
  shows natMin(a, a) = a
proof
  exact natMin.of_le with (LessEqual.reflexive at a)

theorem natMax.self (a : Nat)
  shows natMax(a, a) = a
proof
  exact natMax.of_le with (LessEqual.reflexive at a)

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

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

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

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

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

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

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

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

theorem natMin.le_natMax (a b : Nat)
  shows natMin(a, b) ≤ natMax(a, b)
proof
  have low := natMin.le_left at a, b
  have high := natMax.ge_left at a, b
  exact LessEqual.transitive with low, high

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

theorem natMin.le_iff_or (a b c : Nat)
  shows natMin(a, b) ≤ c ↔ a ≤ c ∨ b ≤ c
proof
  have minNat := natMin.natural at a, b
  constructor
  . intro below
    have split := natMin.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 := natMin.le_left at a, b
      exact LessEqual.transitive with low, first
    . have high := natMin.le_right at a, b
      exact LessEqual.transitive with high, second

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

theorem natMax.ge_iff_or (a b c : Nat)
  shows c ≤ natMax(a, b) ↔ c ≤ a ∨ c ≤ b
proof
  have maxNat := natMax.natural at a, b
  constructor
  . intro below
    have split := natMax.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 := natMax.ge_left at a, b
      exact LessEqual.transitive with first, low
    . have high := natMax.ge_right at a, b
      exact LessEqual.transitive with second, high

theorem natMin.lt_iff (a b c : Nat)
  shows c < natMin(a, b) ↔ c < a ∧ c < b
proof
  have minNat := natMin.natural at a, b
  have low := natMin.le_left at a, b
  have high := natMin.le_right at a, b
  constructor
  . intro below
    constructor
    . exact Less.transitive_LessEqual with below, low
    . exact Less.transitive_LessEqual with below, high
  . intro both
    have total := LessEqual.total at a, b
    cases total with first | second
    . have value113 := natMin.of_le with first
      rw value113
      exact both.left
    . have value114 := natMin.of_ge with second
      rw value114
      exact both.right

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

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

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

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

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

theorem natMin.zero_left (a : Nat)
  shows natMin(0, a) = 0
proof
  have zero : 0 ≤ a by linarith
  exact natMin.of_le with zero

theorem natMin.zero_right (a : Nat)
  shows natMin(a, 0) = 0
proof
  have zero : 0 ≤ a by linarith
  exact natMin.of_ge with zero

theorem natMax.zero_left (a : Nat)
  shows natMax(0, a) = a
proof
  have zero : 0 ≤ a by linarith
  exact natMax.of_le with zero

theorem natMax.zero_right (a : Nat)
  shows natMax(a, 0) = a
proof
  have zero : 0 ≤ a by linarith
  exact natMax.of_ge with zero

theorem natMin.eq_zero_iff (a b : Nat)
  shows natMin(a, b) = 0 ↔ a = 0 ∨ b = 0
proof
  constructor
  . intro zero
    have split := natMin.cases at a, b
    cases split with first | second
    . left
      rw ← first
      exact zero
    . right
      rw ← second
      exact zero
  . intro split
    cases split with first | second
    . rw first
      exact natMin.zero_left with *
    . rw second
      exact natMin.zero_right with *

theorem natMax.eq_zero_iff (a b : Nat)
  shows natMax(a, b) = 0 ↔ a = 0 ∧ b = 0
proof
  constructor
  . intro zero
    have low := natMax.ge_left at a, b
    have high := natMax.ge_right at a, b
    rw zero at low
    rw zero at high
    constructor
    . exact LessEqual.eq_zero with low
    . exact LessEqual.eq_zero with high
  . intro both
    rw [both.left, both.right]
    exact natMax.self with *

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

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

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

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

theorem natMin.add_left (a b k : Nat)
  shows natMin(k + a, k + b) = k + natMin(a, b)
proof
  have total := LessEqual.total at a, b
  cases total with below | above
  . have shifted : k + a ≤ k + b by linarith
    have value13 := natMin.of_le with below
    have value14 := natMin.of_le with shifted
    rw [value13, value14]
    rfl
  . have shifted : k + b ≤ k + a by linarith
    have value15 := natMin.of_ge with above
    have value16 := natMin.of_ge with shifted
    rw [value15, value16]
    rfl

theorem natMin.add_right (a b k : Nat)
  shows natMin(a + k, b + k) = natMin(a, b) + k
proof
  have total := LessEqual.total at a, b
  cases total with below | above
  . have shifted : a + k ≤ b + k by linarith
    have value17 := natMin.of_le with below
    have value18 := natMin.of_le with shifted
    rw [value17, value18]
    rfl
  . have shifted : b + k ≤ a + k by linarith
    have value19 := natMin.of_ge with above
    have value20 := natMin.of_ge with shifted
    rw [value19, value20]
    rfl

theorem natMax.add_left (a b k : Nat)
  shows natMax(k + a, k + b) = k + natMax(a, b)
proof
  have total := LessEqual.total at a, b
  cases total with below | above
  . have shifted : k + a ≤ k + b by linarith
    have value21 := natMax.of_le with below
    have value22 := natMax.of_le with shifted
    rw [value21, value22]
    rfl
  . have shifted : k + b ≤ k + a by linarith
    have value23 := natMax.of_ge with above
    have value24 := natMax.of_ge with shifted
    rw [value23, value24]
    rfl

theorem natMax.add_right (a b k : Nat)
  shows natMax(a + k, b + k) = natMax(a, b) + k
proof
  have total := LessEqual.total at a, b
  cases total with below | above
  . have shifted : a + k ≤ b + k by linarith
    have value25 := natMax.of_le with below
    have value26 := natMax.of_le with shifted
    rw [value25, value26]
    rfl
  . have shifted : b + k ≤ a + k by linarith
    have value27 := natMax.of_ge with above
    have value28 := natMax.of_ge with shifted
    rw [value27, value28]
    rfl

theorem natMin.add_one (a b : Nat)
  shows natMin(a + 1, b + 1) = natMin(a, b) + 1
proof
  exact natMin.add_right at a, b, 1

theorem natMax.add_one (a b : Nat)
  shows natMax(a + 1, b + 1) = natMax(a, b) + 1
proof
  exact natMax.add_right at a, b, 1

theorem natMin.mul_left (a b k : Nat)
  shows natMin(k * a, k * b) = k * natMin(a, b)
proof
  have total := LessEqual.total at a, b
  cases total with below | above
  . have scaled := LessEqual.mul_left at a, b, k with below
    have value29 := natMin.of_le with below
    have value30 := natMin.of_le with scaled
    rw [value29, value30]
    rfl
  . have scaled := LessEqual.mul_left at b, a, k with above
    have value31 := natMin.of_ge with above
    have value32 := natMin.of_ge with scaled
    rw [value31, value32]
    rfl

theorem natMin.mul_right (a b k : Nat)
  shows natMin(a * k, b * k) = natMin(a, b) * k
proof
  have total := LessEqual.total at a, b
  cases total with below | above
  . have scaled := LessEqual.mul_right at a, b, k with below
    have value33 := natMin.of_le with below
    have value34 := natMin.of_le with scaled
    rw [value33, value34]
    rfl
  . have scaled := LessEqual.mul_right at b, a, k with above
    have value35 := natMin.of_ge with above
    have value36 := natMin.of_ge with scaled
    rw [value35, value36]
    rfl

theorem natMax.mul_left (a b k : Nat)
  shows natMax(k * a, k * b) = k * natMax(a, b)
proof
  have total := LessEqual.total at a, b
  cases total with below | above
  . have scaled := LessEqual.mul_left at a, b, k with below
    have value37 := natMax.of_le with below
    have value38 := natMax.of_le with scaled
    rw [value37, value38]
    rfl
  . have scaled := LessEqual.mul_left at b, a, k with above
    have value39 := natMax.of_ge with above
    have value40 := natMax.of_ge with scaled
    rw [value39, value40]
    rfl

theorem natMax.mul_right (a b k : Nat)
  shows natMax(a * k, b * k) = natMax(a, b) * k
proof
  have total := LessEqual.total at a, b
  cases total with below | above
  . have scaled := LessEqual.mul_right at a, b, k with below
    have value41 := natMax.of_le with below
    have value42 := natMax.of_le with scaled
    rw [value41, value42]
    rfl
  . have scaled := LessEqual.mul_right at b, a, k with above
    have value43 := natMax.of_ge with above
    have value44 := natMax.of_ge with scaled
    rw [value43, value44]
    rfl

theorem natMin.add_natMax (a b : Nat)
  shows natMin(a, b) + natMax(a, b) = a + b
proof
  have total := LessEqual.total at a, b
  cases total with below | above
  . have value129 := natMin.of_le with below
    have value130 := natMax.of_le with below
    rw [value129, value130]
    rfl
  . have value131 := natMin.of_ge with above
    have value132 := natMax.of_ge with above
    rw [value131, value132]
    ring

theorem natMax.distribute_natMin (a b c : Nat)
  shows natMax(a, natMin(b, c)) = natMin(natMax(a, b), natMax(a, c))
proof
  have leftNat := natMax.natural at a, b
  have rightNat := natMax.natural at a, c
  have reflexive := LessEqual.reflexive at a
  have total := LessEqual.total at b, c
  cases total with below | above
  . have outer := natMax.monotone at a, b, a, c with reflexive, below
    have value45 := natMin.of_le with below
    have value46 := natMin.of_le with outer
    rw [value45, value46]
    rfl
  . have outer := natMax.monotone at a, c, a, b with reflexive, above
    have value47 := natMin.of_ge with above
    have value48 := natMin.of_ge with outer
    rw [value47, value48]
    rfl

theorem natMin.distribute_natMax (a b c : Nat)
  shows natMin(a, natMax(b, c)) = natMax(natMin(a, b), natMin(a, c))
proof
  have leftNat := natMin.natural at a, b
  have rightNat := natMin.natural at a, c
  have reflexive := LessEqual.reflexive at a
  have total := LessEqual.total at b, c
  cases total with below | above
  . have outer := natMin.monotone at a, b, a, c with reflexive, below
    have value49 := natMax.of_le with below
    have value50 := natMax.of_le with outer
    rw [value49, value50]
    rfl
  . have outer := natMin.monotone at a, c, a, b with reflexive, above
    have value51 := natMax.of_ge with above
    have value52 := natMax.of_ge with outer
    rw [value51, value52]
    rfl

theorem natMin.absorb_natMax (a b : Nat)
  shows natMin(a, natMax(a, b)) = a
proof
  have high := natMax.ge_left at a, b
  exact natMin.of_le with high

theorem natMax.absorb_natMin (a b : Nat)
  shows natMax(a, natMin(a, b)) = a
proof
  have low := natMin.le_left at a, b
  exact natMax.of_ge with low