law min_le_iff

bend-mathlib@0.8.1.0 · nat.bend:1690

import Base

1690# The minimum is at most c exactly when one argument is: min a b <= c tests as a <= c or b <= c.
1691law min_le_iff:
1692  for a: Nat
1693  for b: Nat
1694  for c: Nat
1695  {Nat.is_le(Nat.min(a, b), c) == Bool.or(Nat.is_le(a, c), Nat.is_le(b, c)) : Bool}