law u32_div_to_nat_sym

bend-mathlib@0.8.1.0 · u32.bend:1261

import Base

1261# U32 division is the division of the values, also for a zero divisor: to_nat (a / b) = to_nat a / to_nat b, reversed to rewrite toward the simple side.
1262law u32_div_to_nat_sym:
1263  for a: U32
1264  for b: U32
1265  {Nat.div(U32.to_nat(a), U32.to_nat(b)) == U32.to_nat(U32.div(a, b)) : Nat}