def min_zero

bend-collections-laws-crypto@1.0.0.0 · proofs/math/random/lemire.bend:206

import Base

206def min_zero(+n: Nat) -> {Nat.min(n, 0n) == 0n : Nat}:
207  match n:
208    case 0n:
209      {==}
210    case 1n+p:
211      {==}