def divides_both

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/gcd.bend:65

import Base

65def divides_both(+a: Nat, +b: Nat, +g: Nat, w: Wit) -> Type:
66  {a == Nat.mul(wl(w), g) : Nat} & {b == Nat.mul(wr(w), g) : Nat}