law sub_sub_self

bend-mathlib@0.8.1.0 · nat.bend:2317

import Base

2317# Subtracting a difference from its minuend: m <= n implies n - (n - m) = m.
2318law sub_sub_self:
2319  for n: Nat
2320  for m: Nat
2321  for h: le(m, n)
2322  {Nat.sub(n, Nat.sub(n, m)) == m : Nat}