law max_add_add_right

bend-mathlib@0.8.1.0 · nat.bend:3114

import Base

3114# A common right summand leaves the maximum: max (a + c) (b + c) = max a b + c.
3115law max_add_add_right:
3116  for a: Nat
3117  for b: Nat
3118  for c: Nat
3119  {Nat.max(Nat.add(a, c), Nat.add(b, c)) == Nat.add(Nat.max(a, b), c) : Nat}