law zero_max

bend-mathlib@0.8.1.0 · nat.bend:1055

import Base

1055# Zero is an identity for maximum: max(0, a) = a.
1056law zero_max:
1057  for a: Nat
1058  {Nat.max(0n, a) == a : Nat}