law max_comm

bend-mathlib@0.8.1.0 · nat.bend:975

import Base

975# Maximum is commutative.
976law max_comm:
977  for a: Nat
978  for b: Nat
979  {Nat.max(a, b) == Nat.max(b, a) : Nat}