def factor_parts

bend-collections-laws-math@1.0.0.0 · proofs/math/natural/proof.bend:174

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/natural.bend as S

174# the shared factor g >= 2 and its two quotients, as dvd pairs
175def factor_parts(+a: Nat, +mp: Nat, +g: Nat, +ka: Nat, +km: Nat, p: {Nat.is_le(2n, g) == True{} : Bool} & ({a == Nat.mul(ka, g) : Nat} & {1n+mp == Nat.mul(km, g) : Nat})) -> {Nat.is_le(2n, g) == True{} : Bool} & (S.dvd(g, a) & S.dvd(g, 1n+mp)):
176  (hg, rest) = p
177  (ea, em) = rest
178  (hg, ((ka, ea), (km, em)))