law max_lt_iff_sym

bend-mathlib@0.8.1.0 · nat.bend:4708

import Base

4708# The maximum is below c exactly when both arguments are: max a b < c tests as a < c and b < c, reversed to rewrite toward the simple side.
4709law max_lt_iff_sym:
4710  for a: Nat
4711  for b: Nat
4712  for c: Nat
4713  {Bool.and(Nat.is_lt(a, c), Nat.is_lt(b, c)) == Nat.is_lt(Nat.max(a, b), c) : Bool}