law le_max_iff

bend-mathlib@0.8.1.0 · nat.bend:3208

import Base

3208# 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.
3209law le_max_iff:
3210  for a: Nat
3211  for b: Nat
3212  for c: Nat
3213  {Nat.is_le(a, Nat.max(b, c)) == Bool.or(Nat.is_le(a, b), Nat.is_le(a, c)) : Bool}