Step.low_add: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/random/pcg/step.bend as Step
Lines 44-56 of bend-collections-laws-math@1.0.0.0/proofs/math/random/pcg/step.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/pcg/step.bend&start_line=44&end_line=56

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C

# congruence mod 2^k is kept by sums
def low_add(+k: Nat, +x: Nat, +x2: Nat, +y: Nat, +y2: Nat, +hx: {C.low(k, x) == C.low(k, x2) : Nat}, +hy: {C.low(k, y) == C.low(k, y2) : Nat}) -> {C.low(k, Nat.add(x, y)) == C.low(k, Nat.add(x2, y2)) : Nat}:
  +e1 = Equal.trans(Nat, C.low(k, Nat.add(x, y)), C.low(k, Nat.add(C.low(k, x), y)), C.low(k, Nat.add(C.low(k, x2), y)),
    Equal.sym(Nat, C.low(k, Nat.add(C.low(k, x), y)), C.low(k, Nat.add(x, y)), low_l(k, x, y)),
    Equal.cong(Nat, Nat, z => C.low(k, Nat.add(z, y)), C.low(k, x), C.low(k, x2), hx))
  +e2 = Equal.trans(Nat, C.low(k, Nat.add(C.low(k, x2), y)), C.low(k, Nat.add(x2, y)), C.low(k, Nat.add(x2, C.low(k, y))),
    low_l(k, x2, y),
    Equal.sym(Nat, C.low(k, Nat.add(x2, C.low(k, y))), C.low(k, Nat.add(x2, y)), low_r(k, x2, y)))
  +e3 = Equal.trans(Nat, C.low(k, Nat.add(x2, C.low(k, y))), C.low(k, Nat.add(x2, C.low(k, y2))), C.low(k, Nat.add(x2, y2)),
    Equal.cong(Nat, Nat, z => C.low(k, Nat.add(x2, z)), C.low(k, y), C.low(k, y2), hy),
    low_r(k, x2, y2))
  Equal.trans(Nat, C.low(k, Nat.add(x, y)), C.low(k, Nat.add(C.low(k, x2), y)), C.low(k, Nat.add(x2, y2)), e1,
    Equal.trans(Nat, C.low(k, Nat.add(C.low(k, x2), y)), C.low(k, Nat.add(x2, C.low(k, y))), C.low(k, Nat.add(x2, y2)), e2, e3))

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/pcg/step.bend&name=low_l
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/pcg/step.bend&name=low_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=low