law min_add_add_left

bend-mathlib@0.8.1.0 · nat.bend:3068

import Base

3068# A common left summand leaves the minimum: min (a + b) (a + c) = a + min b c.
3069law min_add_add_left:
3070  for a: Nat
3071  for -b: Nat
3072  for -c: Nat
3073  {Nat.min(Nat.add(a, b), Nat.add(a, c)) == Nat.add(a, Nat.min(b, c)) : Nat}