law le_max_iff_sym

bend-mathlib@0.8.1.0 · nat.bend:4718

import Base

4718# A number is at most the maximum exactly when it is at most one argument: a <= max b c tests as a <= b or a <= c, reversed to rewrite toward the simple side.
4719law le_max_iff_sym:
4720  for a: Nat
4721  for b: Nat
4722  for c: Nat
4723  {Bool.or(Nat.is_le(a, b), Nat.is_le(a, c)) == Nat.is_le(a, Nat.max(b, c)) : Bool}