def lcm_wr

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

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

136def lcm_wr(+a: Nat, +b: Nat) -> Nat:
137  match a b:
138    case 0n _:
139      0n
140    case 1n+ap 0n:
141      0n
142    case 1n+ +ap 1n+ +bp:
143      G.wl(G.ws(1n+bp, 1n+ap, 1n+bp))