law lt_min

bend-mathlib@0.8.1.0 · nat.bend:1656

import Base

1656# A number below both bounds is below their minimum: a < b and a < c imply a < min b c.
1657law lt_min:
1658  for a: Nat
1659  for b: Nat
1660  for c: Nat
1661  for hb: lt(a, b)
1662  for hc: lt(a, c)
1663  lt(a, Nat.min(b, c))