law min_add_add_left_sym

bend-mathlib@0.8.1.0 · nat.bend:4648

import Base

4648# A common left summand leaves the minimum: min (a + b) (a + c) = a + min b c, reversed to rewrite toward the simple side.
4649law min_add_add_left_sym:
4650  for a: Nat
4651  for -b: Nat
4652  for -c: Nat
4653  {Nat.add(a, Nat.min(b, c)) == Nat.min(Nat.add(a, b), Nat.add(a, c)) : Nat}