law max_add_add_left_sym

bend-mathlib@0.8.1.0 · nat.bend:4668

import Base

4668# A common left summand leaves the maximum: max (a + b) (a + c) = a + max b c, reversed to rewrite toward the simple side.
4669law max_add_add_left_sym:
4670  for a: Nat
4671  for -b: Nat
4672  for -c: Nat
4673  {Nat.add(a, Nat.max(b, c)) == Nat.max(Nat.add(a, b), Nat.add(a, c)) : Nat}