def min_le_r

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

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

47def min_le_r(+y: Nat, +hi: Nat) -> {Nat.is_le(Nat.min(y, hi), hi) == True{} : Bool}:
48  match y hi:
49    case 0n h0:
50      N.zero_le(h0)
51    case 1n+yp 0n:
52      {==}
53    case 1n+ +yp 1n+ +hp:
54      min_le_r(yp, hp)