law succ_sub_succ_sym

bend-mathlib@0.8.1.0 · nat.bend:4028

import Base

4028# Subtracting successors: (n + 1) - (m + 1) = n - m, reversed to rewrite toward the simple side.
4029law succ_sub_succ_sym:
4030  for -n: Nat
4031  for -m: Nat
4032  {Nat.sub(n, m) == Nat.sub(1n+n, 1n+m) : Nat}