law min_assoc_sym

bend-mathlib@0.8.1.0 · nat.bend:4159

import Base

4159# Minimum is associative, reversed to rewrite toward the simple side.
4160law min_assoc_sym:
4161  for a: Nat
4162  for b: Nat
4163  for c: Nat
4164  {Nat.min(a, Nat.min(b, c)) == Nat.min(Nat.min(a, b), c) : Nat}