def min_left

bend-collections-laws-math@1.0.0.0 · proofs/lib/nat.bend:535

import Base

535def min_left(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.min(a, b) == a : Nat}:
536  match a b:
537    case 0n _:
538      {==}
539    case 1n+ap 0n:
540      Empty.absurd({Nat.min(1n+ap, 0n) == 1n+ap : Nat}, lt_zero_absurd(1n+ap, h))
541    case 1n+ap 1n+bp:
542      succ_cong(Nat.min(ap, bp), ap, min_left(ap, bp, h))