def le_min

bend-collections-laws-math@1.0.0.0 · proofs/math/natural/misc.bend:56

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

56def 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}:
57  match lo y hi:
58    case 0n y0 h0:
59      N.zero_le(Nat.min(y0, h0))
60    case 1n+lp 0n h0:
61      Empty.absurd({Nat.is_le(1n+lp, Nat.min(0n, h0)) == True{} : Bool}, L.false_true(h1))
62    case 1n+lp 1n+yp 0n:
63      Empty.absurd({Nat.is_le(1n+lp, Nat.min(1n+yp, 0n)) == True{} : Bool}, L.false_true(h2))
64    case 1n+ +lp 1n+ +yp 1n+ +hp:
65      le_min(lp, yp, hp, h1, h2)