law min_max_distrib_left

bend-mathlib@0.8.1.0 · nat.bend:3023

import Base

3023# Minimum distributes over maximum on the left: min a (max b c) = max (min a b) (min a c).
3024law min_max_distrib_left:
3025  for a: Nat
3026  for b: Nat
3027  for c: Nat
3028  {Nat.min(a, Nat.max(b, c)) == Nat.max(Nat.min(a, b), Nat.min(a, c)) : Nat}