law sub_fin

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

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

584law sub_fin:
585  for q: Bool
586  for +r: Nat
587  for +d: Nat
588  for +m: Nat
589  for e: {Nat.add(r, scale(q, m)) == Nat.add(d, m) : Nat}
590  for h: MNat.lt(r, m)
591  {r == d : Nat}