def both_l
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/gcd.bend as Gcdimport Base
111def both_l(+a: Nat, +b: Nat, +g: Nat, w: Wit, p: divides_both(a, b, g, w)) -> {a == Nat.mul(wl(w), g) : Nat}:
112 (el, er) = p
113 el
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/gcd.bend as Gcdimport Base
111def both_l(+a: Nat, +b: Nat, +g: Nat, w: Wit, p: divides_both(a, b, g, w)) -> {a == Nat.mul(wl(w), g) : Nat}:
112 (el, er) = p
113 el