def min_pick

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64sqrt.bend:240

import Base

240# Base 2.0.32 opens both words before it compares them.
241def min_pick(+e: U32, +m: U32) -> {U32.min(e, m) == Bool.pick(U32, U32.is_lt(e, m), e, m) : U32}:
242  match e m:
243    case U32{x} U32{y}:
244      {==}