law min_comm

bend-mathlib@0.8.1.0 · nat.bend:957

import Base

957# Minimum is commutative.
958law min_comm:
959  for a: Nat
960  for b: Nat
961  {Nat.min(a, b) == Nat.min(b, a) : Nat}