law nat_divmod_exact

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

import Base

18law nat_divmod_exact:
19  for +g: Nat
20  for +i: Nat
21  for +bp: Nat
22  for h: {Nat.is_lt(i, 1n+bp) == True{} : Bool}
23  {Nat.divmod(Nat.add(Nat.mul(g, 1n+bp), i), 1n+bp) == (g, i) : Nat & Nat}