def minz

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64light.bend:100

import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend as F64light
import Base

100def minz(+r: Nat) -> {Nat.min(r, 0n) == 0n : Nat}:
101  match r:
102    case 0n:
103      {==}
104    case 1n+ +rp:
105      {==}

Uses (2)

Used by (2)