Proof.factor_parts: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/natural/proof.bend as Proof
Lines 174-178 of bend-collections-laws-math@1.0.0.0/proofs/math/natural/proof.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/proof.bend&start_line=174&end_line=178

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

# the shared factor g >= 2 and its two quotients, as dvd pairs
def 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)):
  (hg, rest) = p
  (ea, em) = rest
  (hg, ((ka, ea), (km, em)))

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/natural.bend&name=dvd