law min_assoc

bend-mathlib@0.8.1.0 · nat.bend:1067

import Base

1067# Minimum is associative.
1068law min_assoc:
1069  for a: Nat
1070  for b: Nat
1071  for c: Nat
1072  {Nat.min(Nat.min(a, b), c) == Nat.min(a, Nat.min(b, c)) : Nat}