law u32_max_to_nat

bend-mathlib@0.8.1.0 · u32.bend:764

import Base

764# The U32 maximum is the maximum of the values: to_nat (max a b) = max (to_nat a) (to_nat b).
765law u32_max_to_nat:
766  for a: U32
767  for b: U32
768  {U32.to_nat(U32.max(a, b)) == Nat.max(U32.to_nat(a), U32.to_nat(b)) : Nat}