law add_mod_carry

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

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

438law add_mod_carry:
439  for q: Bool
440  for +r: Nat
441  for +m: Nat
442  for +s: Nat
443  for e: {Nat.add(r, scale(q, m)) == s : Nat}
444  for h: MNat.lt(r, m)
445  {r == Nat.mod(s, m) : Nat}