law nat_round_up

bend-osdev-u32@0.1.0.0 · LAWS_div.bend:25

import Base

25law nat_round_up:
26  for +bp: Nat
27  for +a: Nat
28  {Nat.mul(Nat.div(Nat.add(a, Nat.sub(1n+bp, 1n)), 1n+bp), 1n+bp) == Nat.add(a, Nat.sub(Nat.sub(1n+bp, 1n), Nat.mod(Nat.add(a, Nat.sub(1n+bp, 1n)), 1n+bp))) : Nat}