law lt_min_iff_sym

bend-mathlib@0.8.1.0 · nat.bend:4698

import Base

4698# A number is below the minimum exactly when it is below both: a < min b c tests as a < b and a < c, reversed to rewrite toward the simple side.
4699law lt_min_iff_sym:
4700  for a: Nat
4701  for b: Nat
4702  for c: Nat
4703  {Bool.and(Nat.is_lt(a, b), Nat.is_lt(a, c)) == Nat.is_lt(a, Nat.min(b, c)) : Bool}