def rec_t2_at

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

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/gcd.bend as GD

86def rec_t2_at(+a: Nat, +bp: Nat, +d: Nat, +kn: Nat, +kr: Nat, +en: {1n+bp == Nat.mul(kn, d) : Nat}, +er: {Nat.mod(a, 1n+bp) == Nat.mul(kr, d) : Nat}) -> dvd2(d, a, 1n+bp):
87  ((Nat.add(Nat.mul(Nat.div(a, 1n+bp), kn), kr), GD.dvd_of_mod(bp, a, d, kn, kr, en, er)), (kn, en))