law max_assoc

bend-mathlib@0.8.1.0 · nat.bend:1086

import Base

1086# Maximum is associative.
1087law max_assoc:
1088  for a: Nat
1089  for b: Nat
1090  for c: Nat
1091  {Nat.max(Nat.max(a, b), c) == Nat.max(a, Nat.max(b, c)) : Nat}