def Transfer

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/bgcdnat.bend:34

import Base

34# every common divisor of (x, y), given by its quotients, divides u and v
35def Transfer(+x: Nat, +y: Nat, +u: Nat, +v: Nat) -> Type:
36  @+d: Nat -> @+kx: Nat -> @+ky: Nat -> @+ex: {x == Nat.mul(kx, d) : Nat} -> @+ey: {y == Nat.mul(ky, d) : Nat} -> dvd2(d, u, v)