law zero_min_sym

bend-mathlib@0.8.1.0 · nat.bend:4135

import Base

4135# The minimum with zero is zero: min(0, a) = 0, reversed to rewrite toward the simple side.
4136law zero_min_sym:
4137  for a: Nat
4138  {0n == Nat.min(0n, a) : Nat}