def both_r
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/gcd.bend as Gcdimport Base
115def both_r(+a: Nat, +b: Nat, +g: Nat, w: Wit, p: divides_both(a, b, g, w)) -> {b == Nat.mul(wr(w), g) : Nat}:
116 (el, er) = p
117 er
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/gcd.bend as Gcdimport Base
115def both_r(+a: Nat, +b: Nat, +g: Nat, w: Wit, p: divides_both(a, b, g, w)) -> {b == Nat.mul(wr(w), g) : Nat}:
116 (el, er) = p
117 er