law min_comm_sym

bend-mathlib@0.8.1.0 · nat.bend:4093

import Base

4093# Minimum is commutative, reversed to rewrite toward the simple side.
4094law min_comm_sym:
4095  for a: Nat
4096  for b: Nat
4097  {Nat.min(b, a) == Nat.min(a, b) : Nat}