def minz
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend as F64lightimport Base
100def minz(+r: Nat) -> {Nat.min(r, 0n) == 0n : Nat}:
101 match r:
102 case 0n:
103 {==}
104 case 1n+ +rp:
105 {==}
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend as F64lightimport Base
100def minz(+r: Nat) -> {Nat.min(r, 0n) == 0n : Nat}:
101 match r:
102 case 0n:
103 {==}
104 case 1n+ +rp:
105 {==}