law max_min_distrib_left

bend-mathlib@0.8.1.0 · nat.bend:3044

import Base

3044# Maximum distributes over minimum on the left: max a (min b c) = min (max a b) (max a c).
3045law max_min_distrib_left:
3046  for a: Nat
3047  for b: Nat
3048  for c: Nat
3049  {Nat.max(a, Nat.min(b, c)) == Nat.min(Nat.max(a, b), Nat.max(a, c)) : Nat}