law sub_add_comm

bend-mathlib@0.8.1.0 · nat.bend:3704

import Base

3704# Subtracting from the left summand commutes with adding the right one: k <= n implies (n + m) - k = (n - k) + m.
3705law sub_add_comm:
3706  for n: Nat
3707  for m: Nat
3708  for k: Nat
3709  for h: le(k, n)
3710  {Nat.sub(Nat.add(n, m), k) == Nat.add(Nat.sub(n, k), m) : Nat}