law sub_add_cancel

bend-mathlib@0.8.1.0 · nat.bend:685

import Base

685# If m <= n, subtracting and adding m back gives n: (n - m) + m = n.
686law sub_add_cancel:
687  for n: Nat
688  for m: Nat
689  for h: le(m, n)
690  {Nat.add(Nat.sub(n, m), m) == n : Nat}