law sub_sub

bend-mathlib@0.8.1.0 · nat.bend:706

import Base

706# Subtracting twice is subtracting the sum: (n - m) - k = n - (m + k).
707law sub_sub:
708  for n: Nat
709  for m: Nat
710  for k: Nat
711  {Nat.sub(Nat.sub(n, m), k) == Nat.sub(n, Nat.add(m, k)) : Nat}