law le_min_of_le_of_le

bend-mathlib@0.8.1.0 · nat.bend:3720

import Base

3720# A lower bound of both b and c is a lower bound of their minimum: a <= b and a <= c imply a <= min b c.
3721law le_min_of_le_of_le:
3722  for a: Nat
3723  for b: Nat
3724  for c: Nat
3725  for hb: le(a, b)
3726  for hc: le(a, c)
3727  le(a, Nat.min(b, c))