law max_le

bend-mathlib@0.8.1.0 · nat.bend:2480

import Base

2480# The maximum is at most c exactly when both arguments are: max a b <= c tests as a <= c and b <= c (Mathlib's max_le_iff; the implication is max_le_of_le_of_le).
2481law max_le:
2482  for a: Nat
2483  for b: Nat
2484  for c: Nat
2485  {Nat.is_le(Nat.max(a, b), c) == Bool.and(Nat.is_le(a, c), Nat.is_le(b, c)) : Bool}