law max_add_add_left

bend-mathlib@0.8.1.0 · nat.bend:3099

import Base

3099# A common left summand leaves the maximum: max (a + b) (a + c) = a + max b c.
3100law max_add_add_left:
3101  for a: Nat
3102  for -b: Nat
3103  for -c: Nat
3104  {Nat.max(Nat.add(a, b), Nat.add(a, c)) == Nat.add(a, Nat.max(b, c)) : Nat}