law mul_zero

bend-mathlib@0.8.1.0 · nat.bend:203

import Base

203# Zero absorbs multiplication on the right: x * 0 = 0.
204law mul_zero:
205  for x: Nat
206  {Nat.mul(x, 0n) == 0n : Nat}