law add_no_carry

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

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

421law add_no_carry:
422  for q: Bool
423  for +r: Nat
424  for +m: Nat
425  for +s: Nat
426  for e: {Nat.add(r, scale(q, m)) == s : Nat}
427  for h: MNat.lt(s, m)
428  {r == s : Nat}