def lcm_wl

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

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

126# lcm(a, b) == kl a and lcm(a, b) == kr b   (Mathlib Nat.dvd_lcm_left/right)
127def lcm_wl(+a: Nat, +b: Nat) -> Nat:
128  match a b:
129    case 0n _:
130      0n
131    case 1n+ap 0n:
132      0n
133    case 1n+ +ap 1n+ +bp:
134      G.wr(G.ws(1n+bp, 1n+ap, 1n+bp))