law min_add_add_right_sym

bend-mathlib@0.8.1.0 · nat.bend:4658

import Base

4658# A common right summand leaves the minimum: min (a + c) (b + c) = min a b + c, reversed to rewrite toward the simple side.
4659law min_add_add_right_sym:
4660  for a: Nat
4661  for b: Nat
4662  for c: Nat
4663  {Nat.add(Nat.min(a, b), c) == Nat.min(Nat.add(a, c), Nat.add(b, c)) : Nat}