def mod_mul_add

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64fmod.bend:40

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/natural_division.bend as ND
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/misc.bend as MS

40def mod_mul_add(+q: Nat, +bp: Nat, +y: Nat) -> {Nat.mod(Nat.add(Nat.mul(q, 1n+bp), y), 1n+bp) == Nat.mod(y, 1n+bp) : Nat}:
41  +B = Nat.add(1n, bp)
42  +Qy = Nat.div(y, B)
43  +Ry = Nat.mod(y, B)
44  +e1 = Equal.cong(Nat, Nat, t => Nat.add(Nat.mul(q, B), t), y, Nat.add(Nat.mul(Qy, B), Ry), MS.divmod_eq(y, bp))
45  +e2 = Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(q, B), Nat.mul(Qy, B)), Ry), Nat.add(Nat.mul(q, B), Nat.add(Nat.mul(Qy, B), Ry)), NA.add_assoc(Nat.mul(q, B), Nat.mul(Qy, B), Ry))
46  +e3 = Equal.cong(Nat, Nat, t => Nat.add(t, Ry), Nat.add(Nat.mul(q, B), Nat.mul(Qy, B)), Nat.mul(Nat.add(q, Qy), B), Equal.sym(Nat, Nat.mul(Nat.add(q, Qy), B), Nat.add(Nat.mul(q, B), Nat.mul(Qy, B)), NA.mul_add_right(q, Qy, B)))
47  +ee = Equal.trans(Nat, Nat.add(Nat.mul(q, B), y), Nat.add(Nat.mul(q, B), Nat.add(Nat.mul(Qy, B), Ry)), Nat.add(Nat.mul(Nat.add(q, Qy), B), Ry), e1, Equal.trans(Nat, Nat.add(Nat.mul(q, B), Nat.add(Nat.mul(Qy, B), Ry)), Nat.add(Nat.add(Nat.mul(q, B), Nat.mul(Qy, B)), Ry), Nat.add(Nat.mul(Nat.add(q, Qy), B), Ry), e2, e3))
48  +hR = N.lt_succ_le(Ry, bp, MS.divmod_lt(y, bp))
49  Equal.trans(Nat, Nat.mod(Nat.add(Nat.mul(q, B), y), B), Nat.mod(Nat.add(Nat.mul(Nat.add(q, Qy), B), Ry), B), Ry, Equal.cong(Nat, Nat, t => Nat.mod(t, B), Nat.add(Nat.mul(q, B), y), Nat.add(Nat.mul(Nat.add(q, Qy), B), Ry), ee), ND.remainder(Nat.add(q, Qy), bp, Ry, hR))