law max_assoc_sym

bend-mathlib@0.8.1.0 · nat.bend:4169

import Base

4169# Maximum is associative, reversed to rewrite toward the simple side.
4170law max_assoc_sym:
4171  for a: Nat
4172  for b: Nat
4173  for c: Nat
4174  {Nat.max(a, Nat.max(b, c)) == Nat.max(Nat.max(a, b), c) : Nat}