law succ_sub

bend-mathlib@0.8.1.0 · nat.bend:1760

import Base

1760# Above the subtrahend, a successor subtracts to a successor: b <= a implies (a + 1) - b = (a - b) + 1.
1761law succ_sub:
1762  for a: Nat
1763  for b: Nat
1764  for h: le(b, a)
1765  {Nat.sub(1n+a, b) == 1n+Nat.sub(a, b) : Nat}