law min_max_distrib_left_sym

bend-mathlib@0.8.1.0 · nat.bend:4628

import Base

4628# Minimum distributes over maximum on the left: min a (max b c) = max (min a b) (min a c), reversed to rewrite toward the simple side.
4629law min_max_distrib_left_sym:
4630  for a: Nat
4631  for b: Nat
4632  for c: Nat
4633  {Nat.max(Nat.min(a, b), Nat.min(a, c)) == Nat.min(a, Nat.max(b, c)) : Nat}