law min_add_add_right

bend-mathlib@0.8.1.0 · nat.bend:3083

import Base

3083# A common right summand leaves the minimum: min (a + c) (b + c) = min a b + c.
3084law min_add_add_right:
3085  for a: Nat
3086  for b: Nat
3087  for c: Nat
3088  {Nat.min(Nat.add(a, c), Nat.add(b, c)) == Nat.add(Nat.min(a, b), c) : Nat}