def lt_of_sum

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/rconst.bend:81

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/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend as I

81# a + c = b + d and c < d give b < a
82def lt_of_sum(+a: Nat, +b: Nat, +c: Nat, +d: Nat, +e: {Nat.add(a, c) == Nat.add(b, d) : Nat}, +h: {Nat.is_lt(c, d) == True{} : Bool}) -> {Nat.is_lt(b, a) == True{} : Bool}:
83  +h2 = N.lt_succ_le_succ(c, d, h)
84  +h3 = N.le_add_left(1n+c, d, b, h2)
85  +h4 = I.le_subst_r(Nat.add(b, 1n+c), Nat.add(b, d), Nat.add(a, c), Equal.sym(Nat, Nat.add(a, c), Nat.add(b, d), e), h3)
86  +e2 = Equal.trans(Nat, Nat.add(b, 1n+c), 1n+Nat.add(b, c), Nat.add(c, 1n+b), NA.add_succ(b, c), sc(b, c))
87  +h5 = I.le_subst_l(Nat.add(b, 1n+c), Nat.add(c, 1n+b), Nat.add(a, c), e2, h4)
88  +h6 = I.le_subst_r(Nat.add(c, 1n+b), Nat.add(a, c), Nat.add(c, a), NA.add_comm(a, c), h5)
89  N.succ_le_lt(b, a, le_cancel_l(c, 1n+b, a, h6))