law max_le_max

bend-mathlib@0.8.1.0 · nat.bend:3305

import Base

3305# Maximum is monotone in both arguments: a <= c and b <= d imply max a b <= max c d.
3306law max_le_max:
3307  for a: Nat
3308  for b: Nat
3309  for c: Nat
3310  for d: Nat
3311  for h1: le(a, c)
3312  for h2: le(b, d)
3313  le(Nat.max(a, b), Nat.max(c, d))