def dvd_of_mod

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

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as R

25# d | n and d | a mod n give d | a: a == (q kn + kr) d
26def dvd_of_mod(+bp: Nat, +a: 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}) -> {a == Nat.mul(Nat.add(Nat.mul(Nat.div(a, 1n+bp), kn), kr), d) : Nat}:
27  +q = Nat.div(a, 1n+bp)
28  %Equal.sym(Nat, Nat.mul(Nat.add(Nat.mul(q, kn), kr), d), Nat.add(Nat.mul(Nat.mul(q, kn), d), Nat.mul(kr, d)), A.mul_add_right(Nat.mul(q, kn), kr, d)) : {a == _ : Nat}
29  %Equal.sym(Nat, Nat.mul(Nat.mul(q, kn), d), Nat.mul(q, Nat.mul(kn, d)), A.mul_assoc(q, kn, d)) : {a == Nat.add(_, Nat.mul(kr, d)) : Nat}
30  %Equal.sym(Nat, Nat.mul(kn, d), 1n+bp, Equal.sym(Nat, 1n+bp, Nat.mul(kn, d), en)) : {a == Nat.add(Nat.mul(q, _), Nat.mul(kr, d)) : Nat}
31  %Equal.sym(Nat, Nat.mul(kr, d), Nat.mod(a, 1n+bp), Equal.sym(Nat, Nat.mod(a, 1n+bp), Nat.mul(kr, d), er)) : {a == Nat.add(Nat.mul(q, 1n+bp), _) : Nat}
32  R.dm_eq(bp, a)