def lt_add_succ
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/memory.bend:455
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend as Memory
import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
455def lt_add_succ(+i: Nat, +r: Nat) -> {Nat.is_lt(i, Nat.add(i, 1n+r)) == True{} : Bool}:
456 %Equal.sym(Nat, Nat.add(i, 1n+r), 1n+Nat.add(i, r), N.add_succ(i, r)) : {Nat.is_lt(i, _) == True{} : Bool}
457 N.le_lt_succ(i, Nat.add(i, r), N.le_add_right(i, r))