law min_add_max

bend-mathlib@0.8.1.0 · nat.bend:1105

import Base

1105# The minimum plus the maximum is the sum: min(a, b) + max(a, b) = a + b.
1106law min_add_max:
1107  for a: Nat
1108  for b: Nat
1109  {Nat.add(Nat.min(a, b), Nat.max(a, b)) == Nat.add(a, b) : Nat}