~/jendhub

def Lcm.least

bend-collections-laws-math@1.0.0.0 · spec/math/natural.bend:153

import bend-collections-laws-math@1.0.0.0/spec/math/natural.bend as Natural
import Base
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M

153# the lcm divides every common multiple
154def Lcm.least(+a: Nat, +b: Nat, +m: Nat, +x: Nat, +y: Nat, +ex: {m == Nat.mul(x, a) : Nat}, +ey: {m == Nat.mul(y, b) : Nat}) -> Type:
155  dvd(M.lcm(a, b), m)

Uses (4)

Used by (1)