def sub_lt_sub

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/width.bend:462

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L

462# a < b, c <= a: a - c < b - c
463def sub_lt_sub(+a: Nat, +b: Nat, +c: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}, +hc: {Nat.is_le(c, a) == True{} : Bool}) -> {Nat.is_lt(Nat.sub(a, c), Nat.sub(b, c)) == True{} : Bool}:
464  +ea = N.sub_add(a, c, hc)
465  +eb = N.sub_add(b, c, N.le_trans(c, a, b, hc, N.lt_le(a, b, h)))
466  +h2 = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(c, Nat.sub(b, c))) == True{} : Bool}, a, Nat.add(c, Nat.sub(a, c)), Equal.sym(Nat, Nat.add(c, Nat.sub(a, c)), a, ea), L.subst(Nat, z => {Nat.is_lt(a, z) == True{} : Bool}, b, Nat.add(c, Nat.sub(b, c)), Equal.sym(Nat, Nat.add(c, Nat.sub(b, c)), b, eb), h))
467  Equal.trans(Bool, Nat.is_lt(Nat.sub(a, c), Nat.sub(b, c)), Nat.is_lt(Nat.add(c, Nat.sub(a, c)), Nat.add(c, Nat.sub(b, c))), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(c, Nat.sub(a, c)), Nat.add(c, Nat.sub(b, c))), Nat.is_lt(Nat.sub(a, c), Nat.sub(b, c)), lt_cancel_l(c, Nat.sub(a, c), Nat.sub(b, c))), h2)