def lt_add_pos

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64dm.bend:40

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
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW

40def lt_add_pos(+a: Nat, +c: Nat, +h: {Nat.is_lt(0n, c) == True{} : Bool}) -> {Nat.is_lt(a, Nat.add(a, c)) == True{} : Bool}:
41  +h1 = Equal.trans(Bool, Nat.is_lt(Nat.add(a, 0n), Nat.add(a, c)), Nat.is_lt(0n, c), True{}, WW.lt_cancel_l(a, 0n, c), h)
42  L.subst(Nat, z => {Nat.is_lt(z, Nat.add(a, c)) == True{} : Bool}, Nat.add(a, 0n), a, N.add_zero(a), h1)