law mul_zero_sym

bend-mathlib@0.8.1.0 · nat.bend:3915

import Base

3915# Zero absorbs multiplication on the right: x * 0 = 0, reversed to rewrite toward the simple side.
3916law mul_zero_sym:
3917  for x: Nat
3918  {0n == Nat.mul(x, 0n) : Nat}