law min_le_iff_sym

bend-mathlib@0.8.1.0 · nat.bend:4321

import Base

4321# The minimum is at most c exactly when one argument is: min a b <= c tests as a <= c or b <= c, reversed to rewrite toward the simple side.
4322law min_le_iff_sym:
4323  for a: Nat
4324  for b: Nat
4325  for c: Nat
4326  {Bool.or(Nat.is_le(a, c), Nat.is_le(b, c)) == Nat.is_le(Nat.min(a, b), c) : Bool}