def l_mul

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

import Base
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/lcm.bend as LC

172def l_mul(+m: Nat, +xs: List<&2, Nat>, +ks: List<&2, Nat>, +acc: Nat, +ka: Nat, +ea: {m == Nat.mul(ka, acc) : Nat}, h: mul_with(m, xs, ks)) -> {m == Nat.mul(lw_mul(m, xs, ks, acc, ka), M.lcm_all_go(xs, acc)) : Nat}:
173  match xs ks:
174    case Nil{} Nil{}:
175      ea
176    case Nil{} Con{k, kt}:
177      ea
178    case Con{x, t} Nil{}:
179      Empty.absurd({m == Nat.mul(lw_mul(m, Con{x, t}, Nil{}, acc, ka), M.lcm_all_go(Con{x, t}, acc)) : Nat}, h)
180    case Con{+x, +t} Con{+k, +kt}:
181      (ex, ht) = h
182      l_mul(m, t, kt, M.lcm(acc, x), LC.lcm_dw(acc, x, m, ka, k), LC.lcm_dvd(acc, x, m, ka, k, ea, ex), ht)