law max_le_sym

bend-mathlib@0.8.1.0 · nat.bend:4571

import Base

4571# 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), reversed to rewrite toward the simple side.
4572law max_le_sym:
4573  for a: Nat
4574  for b: Nat
4575  for c: Nat
4576  {Bool.and(Nat.is_le(a, c), Nat.is_le(b, c)) == Nat.is_le(Nat.max(a, b), c) : Bool}