~/jendhub

law le_max_of_le_right

bend-mathlib@0.8.1.0 · nat.bend:3247

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

3247# A bound by the right argument bounds the maximum: a <= c implies a <= max b c.
3248law le_max_of_le_right:
3249  for a: Nat
3250  for b: Nat
3251  for c: Nat
3252  for h: le(a, c)
3253  le(a, Nat.max(b, c))

Uses (5)

Used by (1)