Misc.le_min: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/natural/misc.bend as Misc
Lines 56-65 of bend-collections-laws-math@1.0.0.0/proofs/math/natural/misc.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/misc.bend&start_line=56&end_line=65

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L

def le_min(+lo: Nat, +y: Nat, +hi: Nat, +h1: {Nat.is_le(lo, y) == True{} : Bool}, +h2: {Nat.is_le(lo, hi) == True{} : Bool}) -> {Nat.is_le(lo, Nat.min(y, hi)) == True{} : Bool}:
  match lo y hi:
    case 0n y0 h0:
      N.zero_le(Nat.min(y0, h0))
    case 1n+lp 0n h0:
      Empty.absurd({Nat.is_le(1n+lp, Nat.min(0n, h0)) == True{} : Bool}, L.false_true(h1))
    case 1n+lp 1n+yp 0n:
      Empty.absurd({Nat.is_le(1n+lp, Nat.min(1n+yp, 0n)) == True{} : Bool}, L.false_true(h2))
    case 1n+ +lp 1n+ +yp 1n+ +hp:
      le_min(lp, yp, hp, h1, h2)

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.min
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend&name=false_true
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=zero_le