law div_div

lawful-words@0.1.0.0 · proof_nat.bend:1298

import Base

1298# (a / x) / y = a / (x * y).
1299law div_div:
1300  for +a: Nat
1301  for +x: Nat
1302  for +y: Nat
1303  {Nat.div(Nat.div(a, x), y) == Nat.div(a, Nat.mul(x, y)) : Nat}