law max_le_of_le_of_le

bend-mathlib@0.8.1.0 · nat.bend:3737

import Base

3737# An upper bound of both a and b bounds their maximum: a <= c and b <= c imply max a b <= c.
3738law max_le_of_le_of_le:
3739  for a: Nat
3740  for b: Nat
3741  for c: Nat
3742  for ha: le(a, c)
3743  for hb: le(b, c)
3744  le(Nat.max(a, b), c)