law nat_mul_succ

bend-osdev-u32@0.1.0.0 · LAWS.bend:276

import Base

276law nat_mul_succ:
277  for +x: Nat
278  for +y: Nat
279  {Nat.mul(x, 1n+y) == Nat.add(x, Nat.mul(x, y)) : Nat}