law lt_min_iff

bend-mathlib@0.8.1.0 · nat.bend:3156

import Base

3156# A number is below the minimum exactly when it is below both: a < min b c tests as a < b and a < c.
3157law lt_min_iff:
3158  for a: Nat
3159  for b: Nat
3160  for c: Nat
3161  {Nat.is_lt(a, Nat.min(b, c)) == Bool.and(Nat.is_lt(a, b), Nat.is_lt(a, c)) : Bool}