def sub_t1_at

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

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR

71def sub_t1_at(+a: Nat, +b: Nat, +d: Nat, +kx: Nat, +ky: Nat, +ex: {a == Nat.mul(kx, d) : Nat}, +ey: {b == Nat.mul(ky, d) : Nat}) -> dvd2(d, a, Nat.sub(b, a)):
72  +e1 = Equal.cong(Nat, Nat, t => Nat.sub(t, a), b, Nat.mul(ky, d), ey)
73  +e2 = Equal.cong(Nat, Nat, t => Nat.sub(Nat.mul(ky, d), t), a, Nat.mul(kx, d), ex)
74  +e3 = Equal.sym(Nat, Nat.mul(Nat.sub(ky, kx), d), Nat.sub(Nat.mul(ky, d), Nat.mul(kx, d)), NR.mul_sub(ky, kx, d))
75  ((kx, ex), (Nat.sub(ky, kx), Equal.trans(Nat, Nat.sub(b, a), Nat.sub(Nat.mul(ky, d), a), Nat.mul(Nat.sub(ky, kx), d), e1, Equal.trans(Nat, Nat.sub(Nat.mul(ky, d), a), Nat.sub(Nat.mul(ky, d), Nat.mul(kx, d)), Nat.mul(Nat.sub(ky, kx), d), e2, e3))))