law add_sub_of_le

bend-mathlib@0.8.1.0 · nat.bend:1778

import Base

1778# Adding back what was subtracted restores the number: a <= b implies a + (b - a) = b.
1779law add_sub_of_le:
1780  for a: Nat
1781  for b: Nat
1782  for h: le(a, b)
1783  {Nat.add(a, Nat.sub(b, a)) == b : Nat}