law min_le_max_sym

bend-mathlib@0.8.1.0 · nat.bend:4891

import Base

4891# The minimum of two numbers is at most their maximum, reversed to rewrite toward the simple side.
4892law min_le_max_sym:
4893  for a: Nat
4894  for b: Nat
4895  {True{} == Nat.is_le(Nat.min(a, b), Nat.max(a, b)) : Bool}