law zero_mul

bend-mathlib@0.8.1.0 · nat.bend:215

import Base

215# Zero absorbs multiplication on the left: 0 * x = 0.
216law zero_mul:
217  for -x: Nat
218  {Nat.mul(0n, x) == 0n : Nat}