def digit_zero

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/u32div.bend:51

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/natural_products.bend as PR

51# a zero digit: 2q b + (a + 2 r) == a + 2 (q b + r)
52def digit_zero(+q: Nat, +bn: Nat, +r: Nat, +a: Nat) -> {Nat.add(Nat.mul(Nat.double(q), bn), Nat.add(a, Nat.double(r))) == Nat.add(a, Nat.double(Nat.add(Nat.mul(q, bn), r))) : Nat}:
53  +x = Nat.double(Nat.mul(q, bn))
54  +rhs = Nat.add(a, Nat.double(Nat.add(Nat.mul(q, bn), r)))
55  %Equal.sym(Nat, Nat.mul(Nat.double(q), bn), x, PR.double_product(q, bn)) : {Nat.add(_, Nat.add(a, Nat.double(r))) == rhs : Nat}
56  %NA.add_swap(a, x, Nat.double(r)) : {_ == rhs : Nat}
57  Equal.cong(Nat, Nat, z => Nat.add(a, z), Nat.add(x, Nat.double(r)), Nat.double(Nat.add(Nat.mul(q, bn), r)), N.add_double(Nat.mul(q, bn), r))