law max_add_add_right_sym

bend-mathlib@0.8.1.0 · nat.bend:4678

import Base

4678# A common right summand leaves the maximum: max (a + c) (b + c) = max a b + c, reversed to rewrite toward the simple side.
4679law max_add_add_right_sym:
4680  for a: Nat
4681  for b: Nat
4682  for c: Nat
4683  {Nat.add(Nat.max(a, b), c) == Nat.max(Nat.add(a, c), Nat.add(b, c)) : Nat}