def double_sub

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

import Base
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/math/natural/fact.bend as FA

358def double_sub(+p: Nat, +q: Nat) -> {Nat.sub(Nat.double(p), Nat.double(q)) == Nat.double(Nat.sub(p, q)) : Nat}:
359  +e1 = Equal.trans(Nat, Nat.sub(Nat.double(p), Nat.double(q)), Nat.sub(Nat.mul(2n, p), Nat.double(q)), Nat.sub(Nat.mul(2n, p), Nat.mul(2n, q)), Equal.cong(Nat, Nat, t => Nat.sub(t, Nat.double(q)), Nat.double(p), Nat.mul(2n, p), NA.double_mul(p)), Equal.cong(Nat, Nat, t => Nat.sub(Nat.mul(2n, p), t), Nat.double(q), Nat.mul(2n, q), NA.double_mul(q)))
360  Equal.trans(Nat, Nat.sub(Nat.double(p), Nat.double(q)), Nat.sub(Nat.mul(2n, p), Nat.mul(2n, q)), Nat.double(Nat.sub(p, q)), e1, Equal.trans(Nat, Nat.sub(Nat.mul(2n, p), Nat.mul(2n, q)), Nat.mul(2n, Nat.sub(p, q)), Nat.double(Nat.sub(p, q)), Equal.sym(Nat, Nat.mul(2n, Nat.sub(p, q)), Nat.sub(Nat.mul(2n, p), Nat.mul(2n, q)), FA.mul_sub_left(2n, p, q)), Equal.sym(Nat, Nat.double(Nat.sub(p, q)), Nat.mul(2n, Nat.sub(p, q)), NA.double_mul(Nat.sub(p, q)))))