def min_zero
import bend-collections-laws-math@1.0.0.0/proofs/math/random/lemire.bend as Lemireimport Base
206def min_zero(+n: Nat) -> {Nat.min(n, 0n) == 0n : Nat}:
207 match n:
208 case 0n:
209 {==}
210 case 1n+p:
211 {==}
import bend-collections-laws-math@1.0.0.0/proofs/math/random/lemire.bend as Lemireimport Base
206def min_zero(+n: Nat) -> {Nat.min(n, 0n) == 0n : Nat}:
207 match n:
208 case 0n:
209 {==}
210 case 1n+p:
211 {==}