def digit_one

bend-collections-laws-math@1.0.0.0 · proofs/lib/u32div.bend:40

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

40# a subtracting digit: (1 + 2q) b + d == a + 2 (q b + r) when b + d == a + 2 r
41def digit_one(+q: Nat, +bn: Nat, +r: Nat, +a: Nat, +d: Nat, +h: {Nat.add(bn, d) == Nat.add(a, Nat.double(r)) : Nat}) -> {Nat.add(Nat.mul(1n+Nat.double(q), bn), d) == Nat.add(a, Nat.double(Nat.add(Nat.mul(q, bn), r))) : Nat}:
42  +x = Nat.double(Nat.mul(q, bn))
43  +rhs = Nat.add(a, Nat.double(Nat.add(Nat.mul(q, bn), r)))
44  %Equal.sym(Nat, Nat.mul(Nat.double(q), bn), x, PR.double_product(q, bn)) : {Nat.add(Nat.add(bn, _), d) == rhs : Nat}
45  %Equal.sym(Nat, Nat.add(Nat.add(bn, x), d), Nat.add(Nat.add(bn, d), x), A.add_rot(bn, x, d)) : {_ == rhs : Nat}
46  %N.add_comm(x, Nat.add(bn, d)) : {_ == rhs : Nat}
47  %Equal.sym(Nat, Nat.add(bn, d), Nat.add(a, Nat.double(r)), h) : {Nat.add(x, _) == rhs : Nat}
48  %NA.add_swap(a, x, Nat.double(r)) : {_ == rhs : Nat}
49  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))