law min_lt_iff

bend-mathlib@0.8.1.0 · nat.bend:3130

import Base

3130# The minimum is below c exactly when one argument is: min a b < c tests as a < c or b < c.
3131law min_lt_iff:
3132  for a: Nat
3133  for b: Nat
3134  for c: Nat
3135  {Nat.is_lt(Nat.min(a, b), c) == Bool.or(Nat.is_lt(a, c), Nat.is_lt(b, c)) : Bool}