Gcd.dvd_mod: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/natural/gcd.bend as Gcd
Lines 15-23 of bend-collections-laws-math@1.0.0.0/proofs/math/natural/gcd.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/gcd.bend&start_line=15&end_line=23

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/lemmas/proofs/nat_algebra.bend as A
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as R

# d | a and d | n give d | a mod n: a mod n == (ka - q kn) d, q = a / n
def dvd_mod(+bp: Nat, +a: Nat, +d: Nat, +ka: Nat, +kn: Nat, +ea: {a == Nat.mul(ka, d) : Nat}, +en: {1n+bp == Nat.mul(kn, d) : Nat}) -> {Nat.mod(a, 1n+bp) == Nat.mul(Nat.sub(ka, Nat.mul(Nat.div(a, 1n+bp), kn)), d) : Nat}:
  +q = Nat.div(a, 1n+bp)
  %Equal.sym(Nat, Nat.mul(Nat.sub(ka, Nat.mul(q, kn)), d), Nat.sub(Nat.mul(ka, d), Nat.mul(Nat.mul(q, kn), d)), R.mul_sub(ka, Nat.mul(q, kn), d)) : {Nat.mod(a, 1n+bp) == _ : Nat}
  %Equal.sym(Nat, Nat.mul(Nat.mul(q, kn), d), Nat.mul(q, Nat.mul(kn, d)), A.mul_assoc(q, kn, d)) : {Nat.mod(a, 1n+bp) == Nat.sub(Nat.mul(ka, d), _) : Nat}
  %Equal.sym(Nat, Nat.mul(kn, d), 1n+bp, Equal.sym(Nat, 1n+bp, Nat.mul(kn, d), en)) : {Nat.mod(a, 1n+bp) == Nat.sub(Nat.mul(ka, d), Nat.mul(q, _)) : Nat}
  %Equal.sym(Nat, Nat.mul(ka, d), a, Equal.sym(Nat, a, Nat.mul(ka, d), ea)) : {Nat.mod(a, 1n+bp) == Nat.sub(_, Nat.mul(q, 1n+bp)) : Nat}
  %Equal.sym(Nat, a, Nat.add(Nat.mul(q, 1n+bp), Nat.mod(a, 1n+bp)), R.dm_eq(bp, a)) : {Nat.mod(a, 1n+bp) == Nat.sub(_, Nat.mul(q, 1n+bp)) : Nat}
  Equal.sym(Nat, Nat.sub(Nat.add(Nat.mul(q, 1n+bp), Nat.mod(a, 1n+bp)), Nat.mul(q, 1n+bp)), Nat.mod(a, 1n+bp), N.add_sub_cancel(Nat.mul(q, 1n+bp), Nat.mod(a, 1n+bp)))

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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=Base/base.bend&name=Nat.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=add_sub_cancel
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend&name=dm_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend&name=mul_sub