Lemmas.sub_arith: law of bend-kit-lemmas@0.1.1.0
Import: import bend-kit-lemmas@0.1.1.0/lemmas.bend as Lemmas
Lines 567-574 of bend-kit-lemmas@0.1.1.0/lemmas.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&start_line=567&end_line=574

import Base
import bend-mathlib@0.7.4.0/nat.bend as MNat

law sub_arith:
  for +a: Nat
  for +b: Nat
  for +nb: Nat
  for +m: Nat
  for h: MNat.le(b, a)
  for hn: {1n+Nat.add(nb, b) == m : Nat}
  {1n+Nat.add(a, nb) == Nat.add(Nat.sub(a, b), m) : Nat}

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=add_assoc_sym
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=add_comm
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=add_succ_sym
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=le
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=sub_add_cancel