def sub_sum

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64norm.bend:88

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

88def sub_sum(+A: Nat, +t: Nat, +B: Nat, +hB: {Nat.is_le(B, t) == True{} : Bool}, +hA: {Nat.is_le(t, A) == True{} : Bool}) -> {Nat.add(Nat.sub(A, t), Nat.sub(t, B)) == Nat.sub(A, B) : Nat}:
89  +r = Nat.sub(t, B)
90  +q = Nat.sub(A, t)
91  +et = N.sub_add(t, B, hB)
92  +eA = N.sub_add(A, t, hA)
93  +e1 = Equal.trans(Nat, Nat.sub(A, B), Nat.sub(Nat.add(t, q), B), Nat.add(q, r), Equal.cong(Nat, Nat, z => Nat.sub(z, B), A, Nat.add(t, q), Equal.sym(Nat, Nat.add(t, q), A, eA)), Equal.trans(Nat, Nat.sub(Nat.add(t, q), B), Nat.sub(Nat.add(Nat.add(B, r), q), B), Nat.add(q, r), Equal.cong(Nat, Nat, z => Nat.sub(Nat.add(z, q), B), t, Nat.add(B, r), Equal.sym(Nat, Nat.add(B, r), t, et)), Equal.trans(Nat, Nat.sub(Nat.add(Nat.add(B, r), q), B), Nat.sub(Nat.add(B, Nat.add(r, q)), B), Nat.add(q, r), Equal.cong(Nat, Nat, z => Nat.sub(z, B), Nat.add(Nat.add(B, r), q), Nat.add(B, Nat.add(r, q)), NA.add_assoc(B, r, q)), Equal.trans(Nat, Nat.sub(Nat.add(B, Nat.add(r, q)), B), Nat.add(r, q), Nat.add(q, r), N.add_sub_cancel(B, Nat.add(r, q)), NA.add_comm(r, q)))))
94  Equal.sym(Nat, Nat.sub(A, B), Nat.add(q, r), e1)