law div_add_mul

lawful-words@0.1.0.0 · proof_nat.bend:1198

import Base

1198law div_add_mul:
1199  for +j: Nat
1200  for +x: Nat
1201  for +z: Nat
1202  for +h: {Nat.is_lt(0n, x) == True{} : Bool}
1203  {Nat.div(Nat.add(Nat.mul(j, x), z), x) == Nat.add(j, Nat.div(z, x)) : Nat}