law max_comm_sym

bend-mathlib@0.8.1.0 · nat.bend:4102

import Base

4102# Maximum is commutative, reversed to rewrite toward the simple side.
4103law max_comm_sym:
4104  for a: Nat
4105  for b: Nat
4106  {Nat.max(b, a) == Nat.max(a, b) : Nat}