law u32_min_to_nat

bend-mathlib@0.8.1.0 · u32.bend:746

import Base

746# The U32 minimum is the minimum of the values: to_nat (min a b) = min (to_nat a) (to_nat b).
747law u32_min_to_nat:
748  for a: U32
749  for b: U32
750  {U32.to_nat(U32.min(a, b)) == Nat.min(U32.to_nat(a), U32.to_nat(b)) : Nat}