def sub1_lt

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

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

198def sub1_lt(+q: Nat, +hq1: {Nat.is_le(1n, q) == True{} : Bool}) -> {Nat.is_lt(Nat.sub(q, 1n), q) == True{} : Bool}:
199  match q:
200    case 0n:
201      Empty.absurd({Nat.is_lt(Nat.sub(0n, 1n), 0n) == True{} : Bool}, L.false_true(hq1))
202    case 1n+ +k:
203      %Equal.sym(Nat, Nat.sub(k, 0n), k, N.sub_zero(k)) : {Nat.is_lt(_, 1n+k) == True{} : Bool}
204      N.lt_succ(k)