law zero_max_sym

bend-mathlib@0.8.1.0 · nat.bend:4151

import Base

4151# Zero is an identity for maximum: max(0, a) = a, reversed to rewrite toward the simple side.
4152law zero_max_sym:
4153  for a: Nat
4154  {a == Nat.max(0n, a) : Nat}