law u32_div_to_nat

bend-mathlib@0.8.1.0 · u32.bend:944

import Base

944# U32 division is the division of the values, also for a zero divisor: to_nat (a / b) = to_nat a / to_nat b.
945law u32_div_to_nat:
946  for a: U32
947  for b: U32
948  {U32.to_nat(U32.div(a, b)) == Nat.div(U32.to_nat(a), U32.to_nat(b)) : Nat}