Lists.dvd_trans: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/natural/lists.bend as Lists
Lines 53-55 of bend-collections-laws-math@1.0.0.0/proofs/math/natural/lists.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/lists.bend&start_line=53&end_line=55

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A

# (a == k1 b and b == k2 c) gives a == (k1 k2) c
def dvd_trans(+a: Nat, +b: Nat, +c: Nat, +k1: Nat, +k2: Nat, +e1: {a == Nat.mul(k1, b) : Nat}, +e2: {b == Nat.mul(k2, c) : Nat}) -> {a == Nat.mul(Nat.mul(k1, k2), c) : Nat}:
  Equal.trans(Nat, a, Nat.mul(k1, b), Nat.mul(Nat.mul(k1, k2), c), e1, Equal.trans(Nat, Nat.mul(k1, b), Nat.mul(k1, Nat.mul(k2, c)), Nat.mul(Nat.mul(k1, k2), c), Equal.cong(Nat, Nat, z => Nat.mul(k1, z), b, Nat.mul(k2, c), e2), Equal.sym(Nat, Nat.mul(Nat.mul(k1, k2), c), Nat.mul(k1, Nat.mul(k2, c)), A.mul_assoc(k1, k2, c))))

Uses (6):
  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.mul
  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