law min_le_max

bend-mathlib@0.8.1.0 · nat.bend:3774

import Base

3774# The minimum of two numbers is at most their maximum.
3775law min_le_max:
3776  for a: Nat
3777  for b: Nat
3778  {Nat.is_le(Nat.min(a, b), Nat.max(a, b)) == True{} : Bool}