law min_lt_iff_sym

bend-mathlib@0.8.1.0 · nat.bend:4688

import Base

4688# The minimum is below c exactly when one argument is: min a b < c tests as a < c or b < c, reversed to rewrite toward the simple side.
4689law min_lt_iff_sym:
4690  for a: Nat
4691  for b: Nat
4692  for c: Nat
4693  {Bool.or(Nat.is_lt(a, c), Nat.is_lt(b, c)) == Nat.is_lt(Nat.min(a, b), c) : Bool}