def lcm_dvd

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/lcm.bend:221

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

221# every common multiple of a and b is a multiple of lcm(a, b)   (Mathlib Nat.lcm_dvd)
222def lcm_dvd(+a: Nat, +b: Nat, +m: Nat, +x: Nat, +y: Nat, +ex: {m == Nat.mul(x, a) : Nat}, +ey: {m == Nat.mul(y, b) : Nat}) -> {m == Nat.mul(lcm_dw(a, b, m, x, y), M.lcm(a, b)) : Nat}:
223  match a b:
224    case 0n b0:
225      Equal.trans(Nat, m, Nat.mul(x, 0n), 0n, ex, A.mul_zero(x))
226    case 1n+ ap 0n:
227      Equal.trans(Nat, m, Nat.mul(y, 0n), 0n, ey, A.mul_zero(y))
228    case 1n+ +ap 1n+ +bp:
229      lcm_dvd_pos(ap, bp, m, x, y, ex, ey)