law max_zero_sym

bend-mathlib@0.8.1.0 · nat.bend:4143

import Base

4143# Zero is an identity for maximum: max(a, 0) = a, reversed to rewrite toward the simple side.
4144law max_zero_sym:
4145  for a: Nat
4146  {a == Nat.max(a, 0n) : Nat}