def lt_succ_le

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/ineq.bend:61

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

61# a < b gives a + 1 <= b
62def lt_succ_le(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_le(Nat.add(a, 1n), b) == True{} : Bool}:
63  %Equal.sym(Nat, Nat.add(a, 1n), Nat.add(1n, a), NA.add_comm(a, 1n)) : {Nat.is_le(_, b) == True{} : Bool}
64  N.lt_succ_le_succ(a, b, h)