law max_lt_iff

bend-mathlib@0.8.1.0 · nat.bend:3182

import Base

3182# The maximum is below c exactly when both arguments are: max a b < c tests as a < c and b < c.
3183law max_lt_iff:
3184  for a: Nat
3185  for b: Nat
3186  for c: Nat
3187  {Nat.is_lt(Nat.max(a, b), c) == Bool.and(Nat.is_lt(a, c), Nat.is_lt(b, c)) : Bool}