def lt_plus

bend-collections-laws-crypto@1.0.0.0 · proofs/math/random/below.bend:46

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WI

46# a < n + a for n > 0
47def lt_plus(+a: Nat, +n: Nat, +hn: {Nat.is_lt(0n, n) == True{} : Bool}) -> {Nat.is_lt(a, Nat.add(n, a)) == True{} : Bool}:
48  Equal.trans(Bool, Nat.is_lt(a, Nat.add(n, a)), Nat.is_lt(0n, n), True{}, WI.lt_cancel_r(0n, n, a), hn)