law zero_mul_sym

bend-mathlib@0.8.1.0 · nat.bend:3923

import Base

3923# Zero absorbs multiplication on the left: 0 * x = 0, reversed to rewrite toward the simple side.
3924law zero_mul_sym:
3925  for -x: Nat
3926  {0n == Nat.mul(0n, x) : Nat}