def le_shift

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/fill.bend:217

import Base
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/crypto/argon2/memory.bend as MEM

217def le_shift(+a: Nat, +r: Nat, +n: Nat, +h: {Nat.is_le(Nat.add(a, 1n+r), n) == True{} : Bool}) -> {Nat.is_le(Nat.add(Nat.add(a, 1n), r), n) == True{} : Bool}:
218  L.subst(Nat, z => {Nat.is_le(z, n) == True{} : Bool}, Nat.add(a, 1n+r), Nat.add(Nat.add(a, 1n), r), Equal.sym(Nat, Nat.add(Nat.add(a, 1n), r), Nat.add(a, 1n+r), MEM.add_one_assoc(a, r)), h)