law min_le_min

bend-mathlib@0.8.1.0 · nat.bend:3286

import Base

3286# Minimum is monotone in both arguments: a <= c and b <= d imply min a b <= min c d.
3287law min_le_min:
3288  for a: Nat
3289  for b: Nat
3290  for c: Nat
3291  for d: Nat
3292  for h1: le(a, c)
3293  for h2: le(b, d)
3294  le(Nat.min(a, b), Nat.min(c, d))