def le_mul_left

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

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

168def le_mul_left(+p: Nat, +q: Nat, +hp: {Nat.is_le(1n, p) == True{} : Bool}) -> {Nat.is_le(q, Nat.mul(p, q)) == True{} : Bool}:
169  match p:
170    case 0n:
171      Empty.absurd({Nat.is_le(q, 0n) == True{} : Bool}, L.false_true(hp))
172    case 1n+k:
173      N.le_add_right(q, Nat.mul(k, q))