law u32_max_to_nat_sym

bend-mathlib@0.8.1.0 · u32.bend:1252

import Base

1252# The U32 maximum is the maximum of the values: to_nat (max a b) = max (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
1253law u32_max_to_nat_sym:
1254  for a: U32
1255  for b: U32
1256  {Nat.max(U32.to_nat(a), U32.to_nat(b)) == U32.to_nat(U32.max(a, b)) : Nat}