law lt_max_iff

bend-mathlib@0.8.1.0 · nat.bend:1716

import Base

1716# The maximum is above a exactly when one argument is: a < max b c tests as a < b or a < c.
1717law lt_max_iff:
1718  for a: Nat
1719  for b: Nat
1720  for c: Nat
1721  {Nat.is_lt(a, Nat.max(b, c)) == Bool.or(Nat.is_lt(a, b), Nat.is_lt(a, c)) : Bool}