law u32_min_to_nat_sym

bend-mathlib@0.8.1.0 · u32.bend:1243

import Base

1243# The U32 minimum is the minimum of the values: to_nat (min a b) = min (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
1244law u32_min_to_nat_sym:
1245  for a: U32
1246  for b: U32
1247  {Nat.min(U32.to_nat(a), U32.to_nat(b)) == U32.to_nat(U32.min(a, b)) : Nat}