~/jendhub

law min_le_of_left_le

bend-mathlib@0.8.1.0 · nat.bend:3260

import bend-mathlib@0.8.1.0/nat.bend as Nat
import Base

3260# A bounded left argument bounds the minimum: a <= c implies min a b <= c.
3261law min_le_of_left_le:
3262  for a: Nat
3263  for b: Nat
3264  for c: Nat
3265  for h: le(a, c)
3266  le(Nat.min(a, b), c)

Uses (5)

Used by (1)