def internal_div_step

bend-mathlib@0.8.1.0 · u32.bend:813

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

813def internal_div_step(+k: Nat, +q: Nat, +b: Nat, +r2: Nat, +x: Nat, +r: Nat, -a: Nat, ek: {Nat.add(Nat.mul(k, b), r2) == Nat.add(x, Nat.double(r)) : Nat}, ea: {Nat.add(Nat.mul(q, b), r) == a : Nat}) -> {Nat.add(Nat.mul(Nat.add(k, Nat.double(q)), b), r2) == Nat.add(x, Nat.double(a)) : Nat}:
814  -l = Nat.add(Nat.mul(Nat.add(k, Nat.double(q)), b), r2)
815  %ea : {l == Nat.add(x, Nat.double(_)) : Nat}
816  %MNat.double_add_sym(Nat.mul(q, b), r) : {l == Nat.add(x, _) : Nat}
817  %MNat.double_mul_sym(q, b) : {l == Nat.add(x, Nat.add(_, Nat.double(r))) : Nat}
818  %MNat.add_mul_sym(k, Nat.double(q), b) : {Nat.add(_, r2) == Nat.add(x, Nat.add(Nat.mul(Nat.double(q), b), Nat.double(r))) : Nat}
819  %MNat.add_left_comm(Nat.mul(Nat.double(q), b), x, Nat.double(r)) : {Nat.add(Nat.add(Nat.mul(k, b), Nat.mul(Nat.double(q), b)), r2) == _ : Nat}
820  %ek : {Nat.add(Nat.add(Nat.mul(k, b), Nat.mul(Nat.double(q), b)), r2) == Nat.add(Nat.mul(Nat.double(q), b), _) : Nat}
821  %MNat.add_left_comm(Nat.mul(k, b), Nat.mul(Nat.double(q), b), r2) : {Nat.add(Nat.add(Nat.mul(k, b), Nat.mul(Nat.double(q), b)), r2) == _ : Nat}
822  MNat.add_assoc(Nat.mul(k, b), Nat.mul(Nat.double(q), b), r2)