1	# Base's Nat division by a divisor 1 + bp (every positive divisor), as the
2	# packages' proofs use it: quotient and remainder recompose the dividend,
3	# the remainder is below the divisor, a dividend g (1 + bp) + i with i below
4	# the divisor has quotient g and remainder i, and rounding a up to a
5	# multiple of the divisor adds the slack (1 + bp - 1) - (a + bp) mod (1 + bp).
6	import Base
7	
8	law nat_div_mod:
9	  for +a: Nat
10	  for +bp: Nat
11	  {Nat.add(Nat.mul(Nat.div(a, 1n+bp), 1n+bp), Nat.mod(a, 1n+bp)) == a : Nat}
12	
13	law nat_mod_lt:
14	  for +a: Nat
15	  for +bp: Nat
16	  {Nat.is_lt(Nat.mod(a, 1n+bp), 1n+bp) == True{} : Bool}
17	
18	law 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}
24	
25	law 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}