~/jendhub

law le_max_of_le_left

bend-mathlib@0.8.1.0 · nat.bend:3234

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

3234# A bound by the left argument bounds the maximum: a <= b implies a <= max b c.
3235law le_max_of_le_left:
3236  for a: Nat
3237  for b: Nat
3238  for c: Nat
3239  for h: le(a, b)
3240  le(a, Nat.max(b, c))

Uses (5)

Used by (1)