law add_sub_assoc

bend-mathlib@0.8.1.0 · nat.bend:2301

import Base

2301# Subtracting a part of the right summand: k <= m implies (n + m) - k = n + (m - k).
2302law add_sub_assoc:
2303  for k: Nat
2304  for m: Nat
2305  for h: le(k, m)
2306  for n: Nat
2307  {Nat.sub(Nat.add(n, m), k) == Nat.add(n, Nat.sub(m, k)) : Nat}