law zero_mod_sym

bend-mathlib@0.8.1.0 · nat.bend:4359

import Base

4359# Zero modulo anything is zero: 0 % b = 0, reversed to rewrite toward the simple side.
4360law zero_mod_sym:
4361  for b: Nat
4362  {0n == Nat.mod(0n, b) : Nat}