law max_self

bend-mathlib@0.8.1.0 · nat.bend:1006

import Base

1006# The maximum of a natural and itself is itself.
1007law max_self:
1008  for a: Nat
1009  {Nat.max(a, a) == a : Nat}