law moddbl

lawful-words@0.1.0.0 · proof_word.bend:106

import Base
import lawful-words@0.1.0.0/proof_nat.bend as N

106# (b + 2x) % 2q = b + 2 (x % q).
107law moddbl:
108  for +b: Bool
109  for +x: Nat
110  for +q: Nat
111  for +hq: {Nat.is_lt(0n, q) == True{} : Bool}
112  {Nat.mod(Nat.add(N.bn(b), Nat.double(x)), Nat.double(q)) == Nat.add(N.bn(b), Nat.double(Nat.mod(x, q))) : Nat}