~/jendhub

law min_le_of_right_le

bend-mathlib@0.8.1.0 · nat.bend:3273

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

3273# A bounded right argument bounds the minimum: b <= c implies min a b <= c.
3274law min_le_of_right_le:
3275  for a: Nat
3276  for b: Nat
3277  for c: Nat
3278  for h: le(b, c)
3279  le(Nat.min(a, b), c)

Uses (5)

Used by (1)