law max_min_distrib_left_sym

bend-mathlib@0.8.1.0 · nat.bend:4638

import Base

4638# Maximum distributes over minimum on the left: max a (min b c) = min (max a b) (max a c), reversed to rewrite toward the simple side.
4639law max_min_distrib_left_sym:
4640  for a: Nat
4641  for b: Nat
4642  for c: Nat
4643  {Nat.min(Nat.max(a, b), Nat.max(a, c)) == Nat.max(a, Nat.min(b, c)) : Nat}