law add_sub_cancel_sym

bend-mathlib@0.8.1.0 · nat.bend:4037

import Base

4037# Adding then subtracting m cancels: (n + m) - m = n, reversed to rewrite toward the simple side.
4038law add_sub_cancel_sym:
4039  for n: Nat
4040  for m: Nat
4041  {n == Nat.sub(Nat.add(n, m), m) : Nat}