law min_add_max_sym

bend-mathlib@0.8.1.0 · nat.bend:4179

import Base

4179# The minimum plus the maximum is the sum: min(a, b) + max(a, b) = a + b, reversed to rewrite toward the simple side.
4180law min_add_max_sym:
4181  for a: Nat
4182  for b: Nat
4183  {Nat.add(a, b) == Nat.add(Nat.min(a, b), Nat.max(a, b)) : Nat}