law max_zero

bend-mathlib@0.8.1.0 · nat.bend:1043

import Base

1043# Zero is an identity for maximum: max(a, 0) = a.
1044law max_zero:
1045  for a: Nat
1046  {Nat.max(a, 0n) == a : Nat}