law sub_arith

bend-kit-lemmas@0.1.1.0 · lemmas.bend:567

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

567law sub_arith:
568  for +a: Nat
569  for +b: Nat
570  for +nb: Nat
571  for +m: Nat
572  for h: MNat.le(b, a)
573  for hn: {1n+Nat.add(nb, b) == m : Nat}
574  {1n+Nat.add(a, nb) == Nat.add(Nat.sub(a, b), m) : Nat}