def g_nth

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/lists.bend:82

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/gcd.bend as G

82def g_nth(+xs: List<&2, Nat>, +acc: Nat, +i: Nat) -> {nth0(xs, i, 0n) == Nat.mul(gw_nth(xs, acc, i), M.gcd_all_go(xs, acc)) : Nat}:
83  match xs i:
84    case Nil{} i0:
85      {==}
86    case Con{+x, +t} 0n:
87      dvd_trans(x, M.gcd(acc, x), M.gcd_all_go(t, M.gcd(acc, x)), G.wr(G.ws(x, acc, x)), gw_acc(t, M.gcd(acc, x)), G.gcd_dvd_right(acc, x), g_acc(t, M.gcd(acc, x)))
88    case Con{+x, +t} 1n+ +j:
89      g_nth(t, M.gcd(acc, x), j)