Grace/Cumulus/Int/MinMax.g17

Open in Workbench Download source

Imports

AbsoluteValueOrder

Declarations

Source

1-- Minimum and maximum of two integers2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Int.MinMax8import AbsoluteValueOrder910theorem integerLess.or_le (x y : Integer)11  shows x < y ∨ y ≤ x12proof13  have split : x < y ∨ ¬x < y by tauto14  cases split with less | notLess15  . left16    exact less17  . right18    exact integerLe.of_not_less with notLess1920defunique integerMin (a b : Set) (m ∈ ℤ) :=21  (integerLe(a, b) ∧ m = a) ∨ (integerLess(b, a) ∧ m = b)22requires aInteger : Integer(a)23requires bInteger : Integer(b)24proof25  have split := integerLess.or_le at b, a26  cases split with above | below27  . have bMember : b ∈ ℤ by settle with Integer28    refine ⟨b, bMember, ?_⟩29    right30    exact ⟨above, rfl⟩31  . have aMember : a ∈ ℤ by settle with Integer32    refine ⟨a, aMember, ?_⟩33    left34    exact ⟨below, rfl⟩3536uniqueness37  intros m mMember first n nMember second38  cases first with firstLow | firstHigh39  . cases second with secondLow | secondHigh40    . cc41    . exfalso42      exact integerLe.not_less with firstLow.left, secondHigh.left43  . cases second with secondLow | secondHigh44    . exfalso45      exact integerLe.not_less with secondLow.left, firstHigh.left46    . cc4748defunique integerMax (a b : Set) (m ∈ ℤ) :=49  (integerLe(a, b) ∧ m = b) ∨ (integerLess(b, a) ∧ m = a)50requires aInteger : Integer(a)51requires bInteger : Integer(b)52proof53  have split := integerLess.or_le at b, a54  cases split with above | below55  . have aMember : a ∈ ℤ by settle with Integer56    refine ⟨a, aMember, ?_⟩57    right58    exact ⟨above, rfl⟩59  . have bMember : b ∈ ℤ by settle with Integer60    refine ⟨b, bMember, ?_⟩61    left62    exact ⟨below, rfl⟩6364uniqueness65  intros m mMember first n nMember second66  cases first with firstLow | firstHigh67  . cases second with secondLow | secondHigh68    . cc69    . exfalso70      exact integerLe.not_less with firstLow.left, secondHigh.left71  . cases second with secondLow | secondHigh72    . exfalso73      exact integerLe.not_less with secondLow.left, firstHigh.left74    . cc7576theorem integerMin.integer (a b : Integer)77  shows Integer(integerMin(a, b))78proof79  have selected := integerMin.selected at a, b with *80  exact selected.left8182theorem integerMax.integer (a b : Integer)83  shows Integer(integerMax(a, b))84proof85  have selected := integerMax.selected at a, b with *86  exact selected.left8788theorem integerMin.of_le (a b : Integer)89  requires below : a ≤ b90  shows integerMin(a, b) = a91proof92  have selected := integerMin.selected at a, b with *93  rcases selected with ⟨member, property⟩94  cases property with low | high95  . exact low.right96  . exfalso97    exact integerLe.not_less with below, high.left9899theorem integerMin.of_ge (a b : Integer)100  requires above : b ≤ a101  shows integerMin(a, b) = b102proof103  have selected := integerMin.selected at a, b with *104  rcases selected with ⟨member, property⟩105  cases property with low | high106  . have same := integerLe.antisymmetric with low.left, above107    rw low.right108    exact same109  . exact high.right110111theorem integerMax.of_le (a b : Integer)112  requires below : a ≤ b113  shows integerMax(a, b) = b114proof115  have selected := integerMax.selected at a, b with *116  rcases selected with ⟨member, property⟩117  cases property with low | high118  . exact low.right119  . exfalso120    exact integerLe.not_less with below, high.left121122theorem integerMax.of_ge (a b : Integer)123  requires above : b ≤ a124  shows integerMax(a, b) = a125proof126  have selected := integerMax.selected at a, b with *127  rcases selected with ⟨member, property⟩128  cases property with low | high129  . have same := integerLe.antisymmetric with low.left, above130    rw low.right131    symm132    exact same133  . exact high.right134135theorem integerMin.self (a : Integer)136  shows integerMin(a, a) = a137proof138  exact integerMin.of_le with (integerLe.reflexive at a)139140theorem integerMax.self (a : Integer)141  shows integerMax(a, a) = a142proof143  exact integerMax.of_le with (integerLe.reflexive at a)144145theorem integerMin.commutative (a b : Integer)146  shows integerMin(a, b) = integerMin(b, a)147proof148  have total := integerLe.total at a, b149  cases total with below | above150  . have left := integerMin.of_le with below151    have right := integerMin.of_ge at b, a with below152    rw [left, right]153    rfl154  . have left := integerMin.of_ge with above155    have right := integerMin.of_le at b, a with above156    rw [left, right]157    rfl158159theorem integerMax.commutative (a b : Integer)160  shows integerMax(a, b) = integerMax(b, a)161proof162  have total := integerLe.total at a, b163  cases total with below | above164  . have left := integerMax.of_le with below165    have right := integerMax.of_ge at b, a with below166    rw [left, right]167    rfl168  . have left := integerMax.of_ge with above169    have right := integerMax.of_le at b, a with above170    rw [left, right]171    rfl172173theorem integerMin.cases (a b : Integer)174  shows integerMin(a, b) = a ∨ integerMin(a, b) = b175proof176  have total := integerLe.total at a, b177  cases total with below | above178  . left179    exact integerMin.of_le with below180  . right181    exact integerMin.of_ge with above182183theorem integerMax.cases (a b : Integer)184  shows integerMax(a, b) = a ∨ integerMax(a, b) = b185proof186  have total := integerLe.total at a, b187  cases total with below | above188  . right189    exact integerMax.of_le with below190  . left191    exact integerMax.of_ge with above192193theorem integerMin.le_left (a b : Integer)194  shows integerMin(a, b) ≤ a195proof196  have total := integerLe.total at a, b197  cases total with below | above198  . have value101 := integerMin.of_le with below199    rw value101200    exact integerLe.reflexive with *201  . have value102 := integerMin.of_ge with above202    rw value102203    exact above204205theorem integerMin.le_right (a b : Integer)206  shows integerMin(a, b) ≤ b207proof208  have total := integerLe.total at a, b209  cases total with below | above210  . have value103 := integerMin.of_le with below211    rw value103212    exact below213  . have value104 := integerMin.of_ge with above214    rw value104215    exact integerLe.reflexive with *216217theorem integerMax.ge_left (a b : Integer)218  shows a ≤ integerMax(a, b)219proof220  have total := integerLe.total at a, b221  cases total with below | above222  . have value105 := integerMax.of_le with below223    rw value105224    exact below225  . have value106 := integerMax.of_ge with above226    rw value106227    exact integerLe.reflexive with *228229theorem integerMax.ge_right (a b : Integer)230  shows b ≤ integerMax(a, b)231proof232  have total := integerLe.total at a, b233  cases total with below | above234  . have value107 := integerMax.of_le with below235    rw value107236    exact integerLe.reflexive with *237  . have value108 := integerMax.of_ge with above238    rw value108239    exact above240241theorem integerMin.le_integerMax (a b : Integer)242  shows integerLe(integerMin(a, b), integerMax(a, b))243proof244  have low := integerMin.le_left at a, b245  have high := integerMax.ge_left at a, b246  exact integerLe.transitive with low, high247248theorem integerMin.le_iff (a b c : Integer)249  shows c ≤ integerMin(a, b) ↔ c ≤ a ∧ c ≤ b250proof251  have minNat := integerMin.integer at a, b252  have low := integerMin.le_left at a, b253  have high := integerMin.le_right at a, b254  constructor255  . intro below256    constructor257    . exact integerLe.transitive with below, low258    . exact integerLe.transitive with below, high259  . intro both260    have total := integerLe.total at a, b261    cases total with first | second262    . have value109 := integerMin.of_le with first263      rw value109264      exact both.left265    . have value110 := integerMin.of_ge with second266      rw value110267      exact both.right268269theorem integerMin.le_iff_or (a b c : Integer)270  shows integerMin(a, b) ≤ c ↔ a ≤ c ∨ b ≤ c271proof272  have minNat := integerMin.integer at a, b273  constructor274  . intro below275    have split := integerMin.cases at a, b276    cases split with first | second277    . left278      rw ← first279      exact below280    . right281      rw ← second282      exact below283  . intro split284    cases split with first | second285    . have low := integerMin.le_left at a, b286      exact integerLe.transitive with low, first287    . have high := integerMin.le_right at a, b288      exact integerLe.transitive with high, second289290theorem integerMax.le_iff (a b c : Integer)291  shows integerMax(a, b) ≤ c ↔ a ≤ c ∧ b ≤ c292proof293  have maxNat := integerMax.integer at a, b294  have low := integerMax.ge_left at a, b295  have high := integerMax.ge_right at a, b296  constructor297  . intro below298    constructor299    . exact integerLe.transitive with low, below300    . exact integerLe.transitive with high, below301  . intro both302    have total := integerLe.total at a, b303    cases total with first | second304    . have value111 := integerMax.of_le with first305      rw value111306      exact both.right307    . have value112 := integerMax.of_ge with second308      rw value112309      exact both.left310311theorem integerMax.ge_iff_or (a b c : Integer)312  shows c ≤ integerMax(a, b) ↔ c ≤ a ∨ c ≤ b313proof314  have maxNat := integerMax.integer at a, b315  constructor316  . intro below317    have split := integerMax.cases at a, b318    cases split with first | second319    . left320      rw ← first321      exact below322    . right323      rw ← second324      exact below325  . intro split326    cases split with first | second327    . have low := integerMax.ge_left at a, b328      exact integerLe.transitive with first, low329    . have high := integerMax.ge_right at a, b330      exact integerLe.transitive with second, high331332theorem integerMin.lt_iff (a b c : Integer)333  shows c < integerMin(a, b) ↔ c < a ∧ c < b334proof335  have minNat := integerMin.integer at a, b336  have low := integerMin.le_left at a, b337  have high := integerMin.le_right at a, b338  constructor339  . intro below340    constructor341    . exact integerLess.transitive_le with below, low342    . exact integerLess.transitive_le with below, high343  . intro both344    have total := integerLe.total at a, b345    cases total with first | second346    . have value113 := integerMin.of_le with first347      rw value113348      exact both.left349    . have value114 := integerMin.of_ge with second350      rw value114351      exact both.right352353theorem integerMax.lt_iff (a b c : Integer)354  shows integerMax(a, b) < c ↔ a < c ∧ b < c355proof356  have maxNat := integerMax.integer at a, b357  have low := integerMax.ge_left at a, b358  have high := integerMax.ge_right at a, b359  constructor360  . intro below361    constructor362    . exact integerLe.transitive_less with low, below363    . exact integerLe.transitive_less with high, below364  . intro both365    have total := integerLe.total at a, b366    cases total with first | second367    . have value115 := integerMax.of_le with first368      rw value115369      exact both.right370    . have value116 := integerMax.of_ge with second371      rw value116372      exact both.left373374theorem integerMin.eq_left_iff (a b : Integer)375  shows integerMin(a, b) = a ↔ a ≤ b376proof377  constructor378  . intro same379    have high := integerMin.le_right at a, b380    rw same at high381    exact high382  . intro below383    exact integerMin.of_le with below384385theorem integerMin.eq_right_iff (a b : Integer)386  shows integerMin(a, b) = b ↔ b ≤ a387proof388  constructor389  . intro same390    have low := integerMin.le_left at a, b391    rw same at low392    exact low393  . intro above394    exact integerMin.of_ge with above395396theorem integerMax.eq_left_iff (a b : Integer)397  shows integerMax(a, b) = a ↔ b ≤ a398proof399  constructor400  . intro same401    have high := integerMax.ge_right at a, b402    rw same at high403    exact high404  . intro above405    exact integerMax.of_ge with above406407theorem integerMax.eq_right_iff (a b : Integer)408  shows integerMax(a, b) = b ↔ a ≤ b409proof410  constructor411  . intro same412    have low := integerMax.ge_left at a, b413    rw same at low414    exact low415  . intro below416    exact integerMax.of_le with below417418theorem integerMin.monotone (a b c d : Integer)419  requires first : a ≤ c420  requires second : b ≤ d421  shows integerLe(integerMin(a, b), integerMin(c, d))422proof423  have low := integerMin.le_left at a, b424  have high := integerMin.le_right at a, b425  apply integerMin.le_iff.backward426  constructor427  . exact integerLe.transitive with low, first428  . exact integerLe.transitive with high, second429430theorem integerMax.monotone (a b c d : Integer)431  requires first : a ≤ c432  requires second : b ≤ d433  shows integerLe(integerMax(a, b), integerMax(c, d))434proof435  have low := integerMax.ge_left at c, d436  have high := integerMax.ge_right at c, d437  apply integerMax.le_iff.backward438  constructor439  . exact integerLe.transitive with first, low440  . exact integerLe.transitive with second, high441442theorem integerMin.associative (a b c : Integer)443  shows integerMin(integerMin(a, b), c) = integerMin(a, integerMin(b, c))444proof445  have innerLeft := integerMin.integer at a, b446  have innerRight := integerMin.integer at b, c447  have total := integerLe.total at a, b448  cases total with below | above449  . have value117 := integerMin.of_le with below450    rw value117451    have totalAC := integerLe.total at a, c452    cases totalAC with belowAC | aboveAC453    . have bound : a ≤ integerMin(b, c)454        exact integerMin.le_iff.backward with ⟨below, belowAC⟩455      have value1 := integerMin.of_le with belowAC456      have value2 := integerMin.of_le with bound457      rw [value1, value2]458      rfl459    . have bound : integerMin(b, c) ≤ a460        have inner := integerMin.le_right at b, c461        exact integerLe.transitive with inner, aboveAC462      have value3 := integerMin.of_ge with aboveAC463      have value4 := integerMin.of_ge with bound464      rw [value3, value4]465      have totalBC := integerLe.total at b, c466      cases totalBC with belowBC | aboveBC467      . have value118 := integerMin.of_le with belowBC468        rw value118469        have bound2 : c ≤ b := integerLe.transitive with aboveAC, below470        exact integerLe.antisymmetric with bound2, belowBC471      . have value119 := integerMin.of_ge with aboveBC472        rw value119473        rfl474  . have value120 := integerMin.of_ge with above475    rw value120476    have totalBC := integerLe.total at b, c477    cases totalBC with belowBC | aboveBC478    . have value121 := integerMin.of_le with belowBC479      rw value121480      have value5 := integerMin.of_ge with above481      rw value5482      rfl483    . have value122 := integerMin.of_ge with aboveBC484      rw value122485      have bound : c ≤ a := integerLe.transitive with aboveBC, above486      have value6 := integerMin.of_ge with bound487      rw value6488      rfl489490theorem integerMax.associative (a b c : Integer)491  shows integerMax(integerMax(a, b), c) = integerMax(a, integerMax(b, c))492proof493  have innerLeft := integerMax.integer at a, b494  have innerRight := integerMax.integer at b, c495  have total := integerLe.total at a, b496  cases total with below | above497  . have value123 := integerMax.of_le with below498    rw value123499    have totalBC := integerLe.total at b, c500    cases totalBC with belowBC | aboveBC501    . have value124 := integerMax.of_le with belowBC502      rw value124503      have bound : a ≤ c := integerLe.transitive with below, belowBC504      have value7 := integerMax.of_le with bound505      rw value7506      rfl507    . have value125 := integerMax.of_ge with aboveBC508      rw value125509      have value8 := integerMax.of_le with below510      rw value8511      rfl512  . have value126 := integerMax.of_ge with above513    rw value126514    have totalAC := integerLe.total at a, c515    cases totalAC with belowAC | aboveAC516    . have bound : a ≤ integerMax(b, c)517        have inner := integerMax.ge_right at b, c518        exact integerLe.transitive with belowAC, inner519      have value9 := integerMax.of_le with belowAC520      have value10 := integerMax.of_le with bound521      rw [value9, value10]522      have totalBC := integerLe.total at b, c523      cases totalBC with belowBC | aboveBC524      . have value127 := integerMax.of_le with belowBC525        rw value127526        rfl527      . have value128 := integerMax.of_ge with aboveBC528        rw value128529        have bound2 : b ≤ c := integerLe.transitive with above, belowAC530        exact integerLe.antisymmetric with aboveBC, bound2531    . have bound : integerMax(b, c) ≤ a532        exact integerMax.le_iff.backward with ⟨above, aboveAC⟩533      have value11 := integerMax.of_ge with aboveAC534      have value12 := integerMax.of_ge with bound535      rw [value11, value12]536      rfl537538theorem integerMin.add_left (a b k : Integer)539  shows integerMin(k + a, k + b) = k + integerMin(a, b)540proof541  have total := integerLe.total at a, b542  cases total with below | above543  . have shifted := integerLe.add_left at a, b, k with below544    have value13 := integerMin.of_le with below545    have value14 := integerMin.of_le with shifted546    rw [value13, value14]547    rfl548  . have shifted := integerLe.add_left at b, a, k with above549    have value15 := integerMin.of_ge with above550    have value16 := integerMin.of_ge with shifted551    rw [value15, value16]552    rfl553554theorem integerMin.add_right (a b k : Integer)555  shows integerMin(a + k, b + k) = integerMin(a, b) + k556proof557  have total := integerLe.total at a, b558  cases total with below | above559  . have shifted := integerLe.add_right at a, b, k with below560    have value17 := integerMin.of_le with below561    have value18 := integerMin.of_le with shifted562    rw [value17, value18]563    rfl564  . have shifted := integerLe.add_right at b, a, k with above565    have value19 := integerMin.of_ge with above566    have value20 := integerMin.of_ge with shifted567    rw [value19, value20]568    rfl569570theorem integerMax.add_left (a b k : Integer)571  shows integerMax(k + a, k + b) = k + integerMax(a, b)572proof573  have total := integerLe.total at a, b574  cases total with below | above575  . have shifted := integerLe.add_left at a, b, k with below576    have value21 := integerMax.of_le with below577    have value22 := integerMax.of_le with shifted578    rw [value21, value22]579    rfl580  . have shifted := integerLe.add_left at b, a, k with above581    have value23 := integerMax.of_ge with above582    have value24 := integerMax.of_ge with shifted583    rw [value23, value24]584    rfl585586theorem integerMax.add_right (a b k : Integer)587  shows integerMax(a + k, b + k) = integerMax(a, b) + k588proof589  have total := integerLe.total at a, b590  cases total with below | above591  . have shifted := integerLe.add_right at a, b, k with below592    have value25 := integerMax.of_le with below593    have value26 := integerMax.of_le with shifted594    rw [value25, value26]595    rfl596  . have shifted := integerLe.add_right at b, a, k with above597    have value27 := integerMax.of_ge with above598    have value28 := integerMax.of_ge with shifted599    rw [value27, value28]600    rfl601602theorem integerMin.add_one (a b : Integer)603  shows integerMin(a + 1, b + 1) = integerMin(a, b) + 1604proof605  exact integerMin.add_right at a, b, integerOne606607theorem integerMax.add_one (a b : Integer)608  shows integerMax(a + 1, b + 1) = integerMax(a, b) + 1609proof610  exact integerMax.add_right at a, b, integerOne611612theorem integerMin.add_integerMax (a b : Integer)613  shows integerMin(a, b) + integerMax(a, b) = a + b614proof615  have total := integerLe.total at a, b616  cases total with below | above617  . have value129 := integerMin.of_le with below618    have value130 := integerMax.of_le with below619    rw [value129, value130]620    rfl621  . have value131 := integerMin.of_ge with above622    have value132 := integerMax.of_ge with above623    rw [value131, value132]624    ring625626theorem integerMax.distribute_integerMin (a b c : Integer)627  shows628    integerMax(a, integerMin(b, c)) =629      integerMin(integerMax(a, b), integerMax(a, c))630proof631  have leftNat := integerMax.integer at a, b632  have rightNat := integerMax.integer at a, c633  have reflexive := integerLe.reflexive at a634  have total := integerLe.total at b, c635  cases total with below | above636  . have outer := integerMax.monotone at a, b, a, c with reflexive, below637    have value45 := integerMin.of_le with below638    have value46 := integerMin.of_le with outer639    rw [value45, value46]640    rfl641  . have outer := integerMax.monotone at a, c, a, b with reflexive, above642    have value47 := integerMin.of_ge with above643    have value48 := integerMin.of_ge with outer644    rw [value47, value48]645    rfl646647theorem integerMin.distribute_integerMax (a b c : Integer)648  shows649    integerMin(a, integerMax(b, c)) =650      integerMax(integerMin(a, b), integerMin(a, c))651proof652  have leftNat := integerMin.integer at a, b653  have rightNat := integerMin.integer at a, c654  have reflexive := integerLe.reflexive at a655  have total := integerLe.total at b, c656  cases total with below | above657  . have outer := integerMin.monotone at a, b, a, c with reflexive, below658    have value49 := integerMax.of_le with below659    have value50 := integerMax.of_le with outer660    rw [value49, value50]661    rfl662  . have outer := integerMin.monotone at a, c, a, b with reflexive, above663    have value51 := integerMax.of_ge with above664    have value52 := integerMax.of_ge with outer665    rw [value51, value52]666    rfl667668theorem integerMin.absorb_integerMax (a b : Integer)669  shows integerMin(a, integerMax(a, b)) = a670proof671  have high := integerMax.ge_left at a, b672  exact integerMin.of_le with high673674theorem integerMax.absorb_integerMin (a b : Integer)675  shows integerMax(a, integerMin(a, b)) = a676proof677  have low := integerMin.le_left at a, b678  exact integerMax.of_ge with low679680theorem integerMin.mul_left (a b k : Integer)681  requires nonnegative : 0 ≤ k682  shows integerMin(k * a, k * b) = k * integerMin(a, b)683proof684  have total := integerLe.total at a, b685  cases total with below | above686  . have scaled := integerLe.mul_left at a, b, k with nonnegative, below687    have value1 := integerMin.of_le with below688    have value2 := integerMin.of_le with scaled689    rw [value1, value2]690    rfl691  . have scaled := integerLe.mul_left at b, a, k with nonnegative, above692    have value1 := integerMin.of_ge with above693    have value2 := integerMin.of_ge with scaled694    rw [value1, value2]695    rfl696697theorem integerMax.mul_left (a b k : Integer)698  requires nonnegative : 0 ≤ k699  shows integerMax(k * a, k * b) = k * integerMax(a, b)700proof701  have total := integerLe.total at a, b702  cases total with below | above703  . have scaled := integerLe.mul_left at a, b, k with nonnegative, below704    have value1 := integerMax.of_le with below705    have value2 := integerMax.of_le with scaled706    rw [value1, value2]707    rfl708  . have scaled := integerLe.mul_left at b, a, k with nonnegative, above709    have value1 := integerMax.of_ge with above710    have value2 := integerMax.of_ge with scaled711    rw [value1, value2]712    rfl713714theorem integerMin.neg (a b : Integer)715  shows integerMin(-a, -b) = -integerMax(a, b)716proof717  have total := integerLe.total at a, b718  cases total with below | above719  . have flipped := integerLe.neg.forward with below720    have value1 := integerMin.of_ge at -a, -b with flipped721    have value2 := integerMax.of_le with below722    rw [value1, value2]723    rfl724  . have flipped := integerLe.neg.forward with above725    have value1 := integerMin.of_le at -a, -b with flipped726    have value2 := integerMax.of_ge with above727    rw [value1, value2]728    rfl729730theorem integerMax.neg (a b : Integer)731  shows integerMax(-a, -b) = -integerMin(a, b)732proof733  have total := integerLe.total at a, b734  cases total with below | above735  . have flipped := integerLe.neg.forward with below736    have value1 := integerMax.of_ge at -a, -b with flipped737    have value2 := integerMin.of_le with below738    rw [value1, value2]739    rfl740  . have flipped := integerLe.neg.forward with above741    have value1 := integerMax.of_le at -a, -b with flipped742    have value2 := integerMin.of_ge with above743    rw [value1, value2]744    rfl745746theorem integerAbs.eq_integerMax (z : Integer)747  shows integerAbs(z) = integerMax(z, -z)748proof749  have split := integerLe.cases_sign at z750  cases split with nonnegative | nonpositive751  . have value := integerAbs.of_nonneg with nonnegative752    have negated := integerLe.neg_nonneg_iff.forward at z753    have flipped : -z ≤ z754      have bound := integerLe.neg.forward with nonnegative755      have zero : -integerZero = integerZero by ring756      rw zero at bound757      exact integerLe.transitive with bound, nonnegative758    have maxValue := integerMax.of_ge at z, -z with flipped759    rw [value, maxValue]760    rfl761  . have value := integerAbs.of_nonpos with nonpositive762    have flipped : z ≤ -z763      have bound := integerLe.neg.forward with nonpositive764      have zero : -integerZero = integerZero by ring765      rw zero at bound766      exact integerLe.transitive with nonpositive, bound767    have maxValue := integerMax.of_le at z, -z with flipped768    rw [value, maxValue]769    rfl770771theorem integerMin.le_integerAbs (z : Integer)772  shows integerMin(z, -z) ≤ integerAbs(z)773proof774  have negatedAbs := integerAbs.neg at z775  have low := integerMin.le_left at z, -z776  have bound := integerAbs.le_self at z777  exact integerLe.transitive with low, bound778