law nat_div_div

lawful-words@0.1.0.0 · LAWS.bend:503

import Base

503# Dividing by 2^j then by 2^k is dividing by 2^(j+k).
504law nat_div_div:
505  for a: Nat
506  for x: Nat
507  for y: Nat
508  {Nat.div(Nat.div(a, x), y) == Nat.div(a, Nat.mul(x, y)) : Nat}